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