java-smt icon indicating copy to clipboard operation
java-smt copied to clipboard

Add a Debug Mode

Open baierd opened this issue 2 years ago • 0 comments

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.

baierd avatar Dec 06 '23 09:12 baierd