# HG changeset patch
# User blanchet
# Date 1416500958 -3600
# Node ID fa7c419f04b48acc371100a7ff79e9c95b6e1bb2
# Parent  b29281d6d1dbae25b61c13f39355c61024d7c082
added CVC4 option that helps on JD

diff -r b29281d6d1db -r fa7c419f04b4 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Thu Nov 20 17:29:18 2014 +0100
+++ b/src/HOL/SMT.thy	Thu Nov 20 17:29:18 2014 +0100
@@ -230,7 +230,7 @@
 *}
 
 declare [[cvc3_options = ""]]
-declare [[cvc4_options = "--full-saturate-quant"]]
+declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call"]]
 declare [[veriT_options = ""]]
 declare [[z3_options = ""]]