--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML Tue Oct 26 21:51:04 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML Wed Oct 27 08:58:03 2010 +0200
@@ -29,7 +29,7 @@
(* CVC3 *)
-val cvc3 = {
+fun cvc3 () = {
name = "cvc3",
env_var = "CVC3_SOLVER",
is_remote = true,
@@ -43,7 +43,7 @@
(* Yices *)
-val yices = {
+fun yices () = {
name = "yices",
env_var = "YICES_SOLVER",
is_remote = false,
@@ -75,7 +75,7 @@
|>> outcome_of "unsat" "sat" "unknown" solver_name
end
-val z3 = {
+fun z3 () = {
name = "z3",
env_var = "Z3_SOLVER",
is_remote = true,
@@ -89,8 +89,8 @@
(* overall setup *)
val setup =
- SMT_Solver.add_solver cvc3 #>
- SMT_Solver.add_solver yices #>
- SMT_Solver.add_solver z3
+ SMT_Solver.add_solver (cvc3 ()) #>
+ SMT_Solver.add_solver (yices ()) #>
+ SMT_Solver.add_solver (z3 ())
end