From 750b3b36959588e2a063a5246c04104d2ebea9a7 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Wed, 4 Sep 2013 20:48:01 -0700
Subject: When a codeexpr is used at the top-level in an assume statement, we
 use the alternative existential semantics.

---
 Source/VCExpr/Boogie2VCExpr.cs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'Source/VCExpr')

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 0b92b1c3..e4101d49 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -47,7 +47,7 @@ namespace Microsoft.Boogie.VCExprAST {
     }
   }
 
-  public delegate VCExpr/*!*/ CodeExprConverter(CodeExpr/*!*/ codeExpr, Hashtable/*<Block, VCExprVar!>*//*!*/ blockVariables, List<VCExprLetBinding> bindings);
+  public delegate VCExpr/*!*/ CodeExprConverter(CodeExpr/*!*/ codeExpr, Hashtable/*<Block, VCExprVar!>*//*!*/ blockVariables, List<VCExprLetBinding> bindings, bool isAssumeContext);
 
   public class Boogie2VCExprTranslator : StandardVisitor, ICloneable {
     // Stack on which the various Visit-methods put the result of the translation
@@ -611,7 +611,7 @@ namespace Microsoft.Boogie.VCExprAST {
       Contract.Assert(false);
       throw new cce.UnreachableException();
     }
-    CodeExprConverter codeExprConverter = null;
+    public CodeExprConverter codeExprConverter = null;
     public void SetCodeExprConverter(CodeExprConverter f) {
       this.codeExprConverter = f;
     }
@@ -623,7 +623,7 @@ namespace Microsoft.Boogie.VCExprAST {
 
       Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/();
       List<VCExprLetBinding/*!*/> bindings = new List<VCExprLetBinding/*!*/>();
-      VCExpr e = codeExprConverter(codeExpr, blockVariables, bindings);
+      VCExpr e = codeExprConverter(codeExpr, blockVariables, bindings, false);
       Push(e);
       return codeExpr;
     }
-- 
cgit v1.2.3