# HG changeset patch
# User blanchet
# Date 1401804161 -7200
# Node ID af95a414136ab9b540cbc1f1c493fd7fdde2fa61
# Parent  d42a5c885cd526e0bb8e260aa599df634ce80311
disable hard-to-reconstruct Z3 feature

diff -r d42a5c885cd5 -r af95a414136a src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Jun 03 14:38:41 2014 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Jun 03 16:02:41 2014 +0200
@@ -174,13 +174,11 @@
 
 lemma
   "a \<noteq> b \<and> a \<noteq> c \<and> b \<noteq> c \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b"
-  using [[smt2_oracle=true]] (* FIXME: disable refine_inj_axiom in Z3 *)
   by smt2
 
 lemma
   "(\<forall>x y z. f x y = f x z \<longrightarrow> y = z) \<and> b \<noteq> c \<longrightarrow> f a b \<noteq> f a c"
   "(\<forall>x y z. f x y = f z y \<longrightarrow> x = z) \<and> a \<noteq> d \<longrightarrow> f a b \<noteq> f d b"
-  using [[smt2_oracle=true]] (* FIXME: disable refine_inj_axiom in Z3 *)
   by smt2+
 
 
diff -r d42a5c885cd5 -r af95a414136a src/HOL/Tools/SMT2/smt2_systems.ML
--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Tue Jun 03 14:38:41 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Tue Jun 03 16:02:41 2014 +0200
@@ -125,6 +125,7 @@
 
   fun z3_options ctxt =
     ["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
+     "smt.refine_inj_axioms=false",
      "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)),
      "-smt2"]