Z3 parameters to help it bail out of fruitless searches faster

print _all_ the attributes of an assert this time
add simpletypes to the visitor

1 files changed, 2 insertions, 1 deletions

diff --git a/Source/Provers/Z3/Prover.ssc b/Source/Provers/Z3/Prover.ssc
index a737b0ae..3bcaf15e 100644
--- a/Source/Provers/Z3/Prover.ssc
+++ b/Source/Provers/Z3/Prover.ssc
@@ -70,7 +70,8 @@ namespace Microsoft.Boogie.Z3
         AddOption(parms, "NNF_SK_HACK", "true");

 

         // More or less like MAM=0.

-        AddOption(parms, "QI_EAGER_THRESHOLD", "100");

+        AddOption(parms, "QI_EAGER_THRESHOLD", "5");

+        AddOption(parms, "QI_LAZY_THRESHOLD", "5");

 

         // Make the integer model more diverse by default, speeds up some benchmarks a lot.

         AddOption(parms, "ARITH_RANDOM_INITIAL_VALUE", "true");