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

3 files changed, 15 insertions, 3 deletions

diff --git a/Source/Core/AbsyCmd.ssc b/Source/Core/AbsyCmd.ssc
index de40c2e8..723b40e3 100644
--- a/Source/Core/AbsyCmd.ssc
+++ b/Source/Core/AbsyCmd.ssc
@@ -2022,11 +2022,17 @@ namespace Microsoft.Boogie
     public override void Emit(TokenTextWriter! stream, int level)

     {

       stream.Write(this, level, "assert ");

-      if (this.Attributes != null)

-        this.Attributes.Emit(stream);

+      EmitAttributes(stream);

       this.Expr.Emit(stream);

       stream.WriteLine(";");

     }

+    protected void EmitAttributes(TokenTextWriter! stream)

+    {

+      for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {

+        kv.Emit(stream);

+        stream.Write(" ");

+      }

+    }

     public override void Typecheck(TypecheckingContext! tc)

     {

       Expr.Typecheck(tc);

diff --git a/Source/Core/StandardVisitor.ssc b/Source/Core/StandardVisitor.ssc
index 192ed7a4..a44290e8 100644
--- a/Source/Core/StandardVisitor.ssc
+++ b/Source/Core/StandardVisitor.ssc
@@ -269,6 +269,11 @@ namespace Microsoft.Boogie
       node = (GlobalVariable) this.VisitVariable(node);

       return node; 

     }

+    public virtual SimpleVariable! VisitSimpleVariable(SimpleVariable! node)

+    {

+      node = (SimpleVariable) this.VisitSimpleVariable(node);

+      return node;

+    }

     public virtual GotoCmd! VisitGotoCmd(GotoCmd! node)

     {

       node.labelTargets = this.VisitBlockSeq((!)node.labelTargets);

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");