changeset 59045 | 1da9b8045026 |
parent 59037 | 650dcf624729 |
child 59381 | de4218223e00 |
--- 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 --inst-no-entail"]] +declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant"]] declare [[verit_options = ""]] declare [[z3_options = ""]]