Fix stack overflow introduced in my previous checkin. Make /typeEncoding:m use separate Z3 type per Boogie type

3 files changed, 19 insertions, 18 deletions

diff --git a/Source/Provers/Z3/TypeDeclCollector.cs b/Source/Provers/Z3/TypeDeclCollector.cs
index 5dfa6468..7cdc6f4f 100644
--- a/Source/Provers/Z3/TypeDeclCollector.cs
+++ b/Source/Provers/Z3/TypeDeclCollector.cs
@@ -174,7 +174,18 @@ void ObjectInvariant()
                        + expr + ") (QID bvconv" + bits + ") (EQ " + expr + " x)))");

 

         KnownTypes.Add(type, true);

+        return;

+      }

+

+      if (type.IsBool || type.IsInt)

+        return;

+

+      if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic) {

+        AddDeclaration("(DEFTYPE " + TypeToString(type) + ")");

+        KnownTypes.Add(type, true);

+        return;

       }

+

     }

 

     public override bool Visit(VCExprNAry node, bool arg) {

@@ -235,7 +246,7 @@ void ObjectInvariant()
           decl += ")";

           AddDeclaration(decl);

 

-          if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic) {

+          if (CommandLineOptions.Clo.MonomorphicArrays && !CommandLineOptions.Clo.UseArrayTheory) {

             var sel = SimplifyLikeExprLineariser.SelectOpName(node);

 

             if (!KnownSelectFunctions.ContainsKey(name)) {

@@ -338,18 +349,7 @@ void ObjectInvariant()
         //

       }

 

-      // What happens in base.Visit() just seems wrong. It seems to use some hack to enumerate 

-      // recursive children of current node, which doesn't seem to work for nested store expressions

-      // (the store expressions themselves get skipped).

-      var res = StandardResult(node, arg);

-      foreach (VCExpr n in node)

-      {

-        n.Accept(this, arg);

-      }

-

-      return res;

-

-      // return base.Visit(node, arg);

+      return base.Visit(node, arg);

     }

 

     private string ExtractBuiltin(Function f) {

diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs
index b8a53b9f..84cf0454 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.cs
+++ b/Source/VCExpr/SimplifyLikeLineariser.cs
@@ -264,10 +264,7 @@ Contract.Ensures(Contract.Result<string>() != null);
         return TypeToStringHelper(t);

       else {

         // at this point, only the types U, T, and bitvector types should be left

-        if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic)

-          return "U";

-        else

-          return TypeToStringHelper(t);

+        return TypeToStringHelper(t);

       }

     }

 

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index 1675a3a7..e87b04ce 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -257,7 +257,11 @@ Contract.Requires(node != null);
       Result res = StandardResult(node, arg);

 

 

-      if (node.TypeParamArity == 0) {

+      if (node.TypeParamArity == 0 &&

+          (node.Op == VCExpressionGenerator.AndOp ||

+           node.Op == VCExpressionGenerator.OrOp  ||

+           node.Op == VCExpressionGenerator.ImpliesOp))

+      {

         Contract.Assert(node.Op != null);

         VCExprOp op = node.Op;