added Z3 4.3.2 (unstable) component
authorblanchet
Fri Apr 25 22:13:17 2014 +0200 (2014-04-25)
changeset 567269fba10c97aef
parent 56725 1ca7fd5f83bb
child 56727 75f4fdafb285
added Z3 4.3.2 (unstable) component
Admin/components/components.sha1
Admin/components/main
src/HOL/Tools/SMT2/smt2_systems.ML
     1.1 --- a/Admin/components/components.sha1	Fri Apr 25 22:13:17 2014 +0200
     1.2 +++ b/Admin/components/components.sha1	Fri Apr 25 22:13:17 2014 +0200
     1.3 @@ -88,3 +88,4 @@
     1.4  12ae71acde43bd7bed1e005c43034b208c0cba4c  z3-3.2.tar.gz
     1.5  d94a716502c8503d63952bcb4d4176fac8b28704  z3-4.0.tar.gz
     1.6  86e721296c400ada440e4a9ce11b9e845eec9e25  z3-4.3.0.tar.gz
     1.7 +06b30757ff23aefbc30479785c212685ffd39f4d  z3-4.3.2pre.tar.gz
     2.1 --- a/Admin/components/main	Fri Apr 25 22:13:17 2014 +0200
     2.2 +++ b/Admin/components/main	Fri Apr 25 22:13:17 2014 +0200
     2.3 @@ -12,6 +12,6 @@
     2.4  scala-2.11.0
     2.5  spass-3.8ds
     2.6  z3-3.2-1
     2.7 -z3-4.3.0
     2.8 +z3-4.3.2pre
     2.9  xz-java-1.2-1
    2.10  ProofGeneral-4.2-1
     3.1 --- a/src/HOL/Tools/SMT2/smt2_systems.ML	Fri Apr 25 22:13:17 2014 +0200
     3.2 +++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Fri Apr 25 22:13:17 2014 +0200
     3.3 @@ -127,8 +127,7 @@
     3.4    fun z3_make_command name () = if_z3_non_commercial (make_command name)
     3.5  
     3.6    fun z3_options ctxt =
     3.7 -    ["REFINE_INJ_AXIOM=false" (* not supported by replay *),
     3.8 -     "smt.random_seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
     3.9 +    ["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
    3.10       "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)),
    3.11       "-smt2"]
    3.12