--- a/src/HOL/Tools/refute.ML Mon Dec 07 09:35:18 2009 +0100
+++ b/src/HOL/Tools/refute.ML Mon Dec 07 11:44:49 2009 +0100
@@ -1192,9 +1192,15 @@
val fm_u = (if negate then toFalse else toTrue) (hd intrs)
val fm_ax = PropLogic.all (map toTrue (tl intrs))
val fm = PropLogic.all [#wellformed args, fm_ax, fm_u]
+ val solver =
+ SatSolver.invoke_solver satsolver
+ handle Option.Option =>
+ error ("Unknown SAT solver: " ^ quote satsolver ^
+ ". Available solvers: " ^
+ commas (map (quote o fst) (!SatSolver.solvers)) ^ ".")
in
priority "Invoking SAT solver...";
- (case SatSolver.invoke_solver satsolver fm of
+ (case solver fm of
SatSolver.SATISFIABLE assignment =>
(priority ("*** Model found: ***\n" ^ print_model thy model
(fn i => case assignment i of SOME b => b | NONE => true));