# HG changeset patch
# User boehmes
# Date 1292596200 -3600
# Node ID 975db7bd23e3d4dbf5b31463ec9a7d4e4b7ec313
# Parent  c99ed404cb11980debdfe33ba2b106a0232286b5
fixed the command-line syntax for setting Yices' random seed

diff -r c99ed404cb11 -r 975db7bd23e3 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"),