From 024e1669cac41a45ba0d825035a25d32a1562a67 Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Wed, 18 Aug 2010 00:54:22 +0000
Subject: Fix stack overflow introduced in my previous checkin. Make
 /typeEncoding:m use separate Z3 type per Boogie type

---
 Source/VCExpr/SimplifyLikeLineariser.cs | 5 +----
 Source/VCExpr/VCExprASTVisitors.cs      | 6 +++++-
 2 files changed, 6 insertions(+), 5 deletions(-)

(limited to 'Source/VCExpr')

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;
         
-- 
cgit v1.2.3