# HG changeset patch
# User blanchet
# Date 1398456797 -7200
# Node ID 9fba10c97aefcef53fcfad85e4011b6b2db14057
# Parent  1ca7fd5f83bba98ff0fd8d6a25c3a503e4183f6b
added Z3 4.3.2 (unstable) component

diff -r 1ca7fd5f83bb -r 9fba10c97aef Admin/components/components.sha1
--- a/Admin/components/components.sha1	Fri Apr 25 22:13:17 2014 +0200
+++ b/Admin/components/components.sha1	Fri Apr 25 22:13:17 2014 +0200
@@ -88,3 +88,4 @@
 12ae71acde43bd7bed1e005c43034b208c0cba4c  z3-3.2.tar.gz
 d94a716502c8503d63952bcb4d4176fac8b28704  z3-4.0.tar.gz
 86e721296c400ada440e4a9ce11b9e845eec9e25  z3-4.3.0.tar.gz
+06b30757ff23aefbc30479785c212685ffd39f4d  z3-4.3.2pre.tar.gz
diff -r 1ca7fd5f83bb -r 9fba10c97aef Admin/components/main
--- a/Admin/components/main	Fri Apr 25 22:13:17 2014 +0200
+++ b/Admin/components/main	Fri Apr 25 22:13:17 2014 +0200
@@ -12,6 +12,6 @@
 scala-2.11.0
 spass-3.8ds
 z3-3.2-1
-z3-4.3.0
+z3-4.3.2pre
 xz-java-1.2-1
 ProofGeneral-4.2-1
diff -r 1ca7fd5f83bb -r 9fba10c97aef src/HOL/Tools/SMT2/smt2_systems.ML
--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Fri Apr 25 22:13:17 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Fri Apr 25 22:13:17 2014 +0200
@@ -127,8 +127,7 @@
   fun z3_make_command name () = if_z3_non_commercial (make_command name)
 
   fun z3_options ctxt =
-    ["REFINE_INJ_AXIOM=false" (* not supported by replay *),
-     "smt.random_seed=" ^ 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"]