Several problems with unclear cause (to a user not fimilar with JavaSMT) are encountered on a regular basis when using JavaSMT. An example would be usage of a formula in an context that is distinct to the creation context. Error messages are typically non-descriptive and not helpful (Example: encountered formula of type Bool, but type Bool required).
I propose to add a debug mode to JavaSMT, that tracks certain information that is usally not tracked (e.g. thread of origin and FormulaManager/Object of origin for formulas) and asserts some known information (e.g. usage of formulas only in FormulaManagers of its origin context). This way, a developer or user can find common errors fast and automatically.
Several problems with unclear cause (to a user not fimilar with JavaSMT) are encountered on a regular basis when using JavaSMT. An example would be usage of a formula in an context that is distinct to the creation context. Error messages are typically non-descriptive and not helpful (Example: encountered formula of type Bool, but type Bool required).
I propose to add a debug mode to JavaSMT, that tracks certain information that is usally not tracked (e.g. thread of origin and FormulaManager/Object of origin for formulas) and asserts some known information (e.g. usage of formulas only in FormulaManagers of its origin context). This way, a developer or user can find common errors fast and automatically.