use Z3 4.3.2 syntax
authorblanchet
Fri Apr 25 22:13:17 2014 +0200 (2014-04-25)
changeset 56724faa9c21977d2
parent 56723 a8f71445c265
child 56725 1ca7fd5f83bb
use Z3 4.3.2 syntax
src/HOL/Tools/SMT2/smt2_systems.ML
     1.1 --- a/src/HOL/Tools/SMT2/smt2_systems.ML	Fri Apr 25 21:45:04 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Fri Apr 25 22:13:17 2014 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4  
     1.5    fun z3_options ctxt =
     1.6      ["REFINE_INJ_AXIOM=false" (* not supported by replay *),
     1.7 -     "-rs:" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
     1.8 +     "smt.random_seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
     1.9       "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)),
    1.10       "-smt2"]
    1.11