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