src/HOL/Tools/SMT/smt_failure.ML
Mon, 15 Nov 2010 22:23:28 +0100 boehmes renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
Fri, 12 Nov 2010 17:28:43 +0100 boehmes check the return code of the SMT solver and raise an exception if the prover failed
Fri, 12 Nov 2010 15:56:10 +0100 boehmes 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
Mon, 08 Nov 2010 12:13:44 +0100 boehmes 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)
less more (0) tip