summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/Provers/Z3/Prover.ssc4
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/Provers/Z3/Prover.ssc b/Source/Provers/Z3/Prover.ssc
index 3bcaf15e..44d450c0 100644
--- a/Source/Provers/Z3/Prover.ssc
+++ b/Source/Provers/Z3/Prover.ssc
@@ -70,8 +70,8 @@ namespace Microsoft.Boogie.Z3
AddOption(parms, "NNF_SK_HACK", "true");
// More or less like MAM=0.
- AddOption(parms, "QI_EAGER_THRESHOLD", "5");
- AddOption(parms, "QI_LAZY_THRESHOLD", "5");
+ AddOption(parms, "QI_EAGER_THRESHOLD", "100");
+ // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more.
// Make the integer model more diverse by default, speeds up some benchmarks a lot.
AddOption(parms, "ARITH_RANDOM_INITIAL_VALUE", "true");