src/HOL/Tools/SMT/smt_failure.ML
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'
2010-11-30 boehmes 2010-11-30 split up Z3 models into constraints on free variables and constant definitions; reduce Z3 models by replacing unknowns with free variables and constants from the goal; remove occurrences of the hidden constant fun_app from Z3 models
2010-11-15 boehmes 2010-11-15 renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
2010-11-12 boehmes 2010-11-12 check the return code of the SMT solver and raise an exception if the prover failed
2010-11-12 boehmes 2010-11-12 turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
2010-11-08 boehmes 2010-11-08 better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)