# HG changeset patch
# User blanchet
# Date 1405376492 -7200
# Node ID 2a6c31ac1c9aad6342a5906cb6488dd00187812a
# Parent  1072599c43f649d91b42385e98c5871834b9fec9
don't generate a 'set-logic' command when generating problems in a non-standard (but Z3-supported) union-of-everything logic

diff -r 1072599c43f6 -r 2a6c31ac1c9a src/HOL/Tools/SMT2/smtlib2_interface.ML
--- a/src/HOL/Tools/SMT2/smtlib2_interface.ML	Tue Jul 15 00:21:29 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2_interface.ML	Tue Jul 15 00:21:32 2014 +0200
@@ -77,7 +77,11 @@
   let
     fun choose [] = "AUFLIA"
       | choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs)
-  in "(set-logic " ^ choose (Logics.get (Context.Proof ctxt)) ^ ")\n" end
+  in
+    (case choose (Logics.get (Context.Proof ctxt)) of
+      "" => "" (* for default Z3 logic, a subset of everything *)
+    | logic => "(set-logic " ^ logic ^ ")\n")
+  end
 
 
 (** serialization **)
diff -r 1072599c43f6 -r 2a6c31ac1c9a src/HOL/Word/Tools/smt2_word.ML
--- a/src/HOL/Word/Tools/smt2_word.ML	Tue Jul 15 00:21:29 2014 +0200
+++ b/src/HOL/Word/Tools/smt2_word.ML	Tue Jul 15 00:21:32 2014 +0200
@@ -12,8 +12,10 @@
 
 (* SMT-LIB logic *)
 
+(* "QF_AUFBV" is too restricted for Isabelle's problems, which contain aritmetic and quantifiers.
+   Better set the logic to "" and make at least Z3 happy. *)
 fun smtlib_logic ts =
-  if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "QF_AUFBV" else NONE
+  if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "" else NONE
 
 
 (* SMT-LIB builtins *)