author | blanchet |
Mon, 24 Nov 2014 12:35:13 +0100 | |
changeset 59036 | ce58eb744e38 |
parent 59035 | 3a2153676705 |
child 59037 | 650dcf624729 |
src/HOL/SMT.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/SMT.thy Mon Nov 24 12:35:13 2014 +0100 +++ b/src/HOL/SMT.thy Mon Nov 24 12:35:13 2014 +0100 @@ -230,7 +230,7 @@ *} declare [[cvc3_options = ""]] -declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call"]] +declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail"]] declare [[verit_options = ""]] declare [[z3_options = ""]]