fixed the command-line syntax for setting Yices' random seed
authorboehmes
Fri, 17 Dec 2010 15:30:00 +0100
changeset 41235 975db7bd23e3
parent 41234 c99ed404cb11
child 41244 7c05c8301d7e
fixed the command-line syntax for setting Yices' random seed
src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Fri Dec 17 15:07:32 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Fri Dec 17 15:30:00 2010 +0100
@@ -53,7 +53,7 @@
   env_var = "YICES_SOLVER",
   is_remote = false,
   options = (fn ctxt => [
-    "--rand-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
+    "--rand-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
     "--smtlib"]),
   class = SMTLIB_Interface.smtlibC,
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),