# HG changeset patch
# User blanchet
# Date 1424190165 -3600
# Node ID ae50c9b824440538353a532bf4ea8a8ee0c6be38
# Parent  5283e349b3396bc84c177be95a94c48497668914
use more permissive logic for CVC4 (in case both reals and datatypes appear)

diff -r 5283e349b339 -r ae50c9b82444 src/HOL/Tools/SMT/cvc4_interface.ML
--- a/src/HOL/Tools/SMT/cvc4_interface.ML	Sun Feb 15 17:01:22 2015 +0100
+++ b/src/HOL/Tools/SMT/cvc4_interface.ML	Tue Feb 17 17:22:45 2015 +0100
@@ -19,7 +19,7 @@
 
 local
   fun translate_config ctxt =
-    {logic = K "(set-logic AUFDTLIA)\n", fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
+    {logic = K "(set-logic ALL_SUPPORTED)\n", fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
      serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
 in