# HG changeset patch
# User blanchet
# Date 1398456797 -7200
# Node ID faa9c21977d29d22b83c3ab1d275706eeb3e49bb
# Parent  a8f71445c265743f0bb4d73f3af6c13a335da879
use Z3 4.3.2 syntax

diff -r a8f71445c265 -r faa9c21977d2 src/HOL/Tools/SMT2/smt2_systems.ML
--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Fri Apr 25 21:45:04 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Fri Apr 25 22:13:17 2014 +0200
@@ -128,7 +128,7 @@
 
   fun z3_options ctxt =
     ["REFINE_INJ_AXIOM=false" (* not supported by replay *),
-     "-rs:" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
+     "smt.random_seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
      "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)),
      "-smt2"]