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/VCExprASTVisitors.cs | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'Source/VCExpr/VCExprASTVisitors.cs')

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