diff options
| author |  MichalMoskal <unknown> | 2009-12-10 02:13:04 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2009-12-10 02:13:04 +0000 |
| commit | 0200e36a886f6b4c9d7738ba3286ca6f68be6e78 (patch) | |
| tree | 39c0d59a0e3908da26423c2c3e98c7264e852b7c /Source/Provers | |
| parent | 786e335fbfe03ca283fd9dd784251802f6a88f19 (diff) | |
Revert the matching depth limit change from previous checkin: would break VCC.
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/Z3/Prover.ssc | 4 |
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");
|