# HG changeset patch
# User blanchet
# Date 1394724069 -3600
# Node ID 040424c3800da2190330474e7e48d598f1205722
# Parent  5b76e1790c3845a7714d96c16d38f1b5566d1216
updated SMT2 examples and certificates

diff -r 5b76e1790c38 -r 040424c3800d src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Thu Mar 13 16:17:14 2014 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Thu Mar 13 16:21:09 2014 +0100
@@ -127,7 +127,7 @@
   "\<exists>x. P x \<longrightarrow> P a \<and> P b"
   "\<exists>x. (\<exists>y. P y) \<longrightarrow> P x"
   "(\<exists>x. Q \<longrightarrow> P x) \<longleftrightarrow> (Q \<longrightarrow> (\<exists>x. P x))"
-  by smt2+
+  oops (* smt2 FIXME: requires Z3 4.3.1 *)
 
 lemma
   "(\<not>(\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"
@@ -146,7 +146,7 @@
   "(\<exists>x. \<forall>y. P x \<longleftrightarrow> P y) \<longrightarrow> ((\<exists>x. P x) \<longleftrightarrow> (\<forall>y. P y))"
   "\<exists>z. P z \<longrightarrow> (\<forall>x. P x)"
   "(\<exists>y. \<forall>x. R x y) \<longrightarrow> (\<forall>x. \<exists>y. R x y)"
-  by smt2+
+  by smt+ (* smt2 FIXME: requires Z3 4.3.1 *)
 
 lemma
   "(\<exists>!x. P x) \<longrightarrow> (\<exists>x. P x)"
diff -r 5b76e1790c38 -r 040424c3800d src/HOL/Tools/SMT2/smt2_solver.ML
--- a/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Mar 13 16:17:14 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Mar 13 16:21:09 2014 +0100
@@ -124,7 +124,7 @@
   let
     val options = SMT2_Config.solver_options_of ctxt
     val cmd = command ()
-    val comments = [space_implode " " (cmd @ options)]
+    val comments = [space_implode " " options]
 
     val (str, replay_data as {context=ctxt', ...}) =
       ithms