author | blanchet |
Fri, 25 Apr 2014 22:13:17 +0200 | |
changeset 56724 | faa9c21977d2 |
parent 56723 | a8f71445c265 |
child 56725 | 1ca7fd5f83bb |
--- 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"]