don't generate a 'set-logic' command when generating problems in a non-standard (but Z3-supported) union-of-everything logic

--- 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 **)

--- 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 *)