# HG changeset patch # User blanchet # Date 1416828913 -3600 # Node ID 1da9b8045026bf923aef3f4906e76c1dcb731448 # Parent c04eccae1de80b2c0ffff1b212bf253ea6829e7f added one more CVC4 option that helps Judgment Day (10 theory version) diff -r c04eccae1de8 -r 1da9b8045026 src/HOL/SMT.thy --- 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 = ""]]