src/HOL/Tools/SMT2/smt2_systems.ML
changeset 56724 faa9c21977d2
parent 56467 8d7d6f17c6a7
child 56726 9fba10c97aef
equal deleted inserted replaced
56723:a8f71445c265 56724:faa9c21977d2
   126 local
   126 local
   127   fun z3_make_command name () = if_z3_non_commercial (make_command name)
   127   fun z3_make_command name () = if_z3_non_commercial (make_command name)
   128 
   128 
   129   fun z3_options ctxt =
   129   fun z3_options ctxt =
   130     ["REFINE_INJ_AXIOM=false" (* not supported by replay *),
   130     ["REFINE_INJ_AXIOM=false" (* not supported by replay *),
   131      "-rs:" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
   131      "smt.random_seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
   132      "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)),
   132      "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)),
   133      "-smt2"]
   133      "-smt2"]
   134 
   134 
   135   fun select_class ctxt =
   135   fun select_class ctxt =
   136     if Config.get ctxt z3_extensions then Z3_New_Interface.smtlib2_z3C
   136     if Config.get ctxt z3_extensions then Z3_New_Interface.smtlib2_z3C