From d3e7cf42294a44b53bb7dc29ea24eff85b836bf0 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Fri, 30 Jan 2015 15:07:47 +0100
Subject: Made it produce slightly different passive commands for assignments
 to assumption variables.

---
 Source/VCGeneration/ConditionGeneration.cs | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'Source/VCGeneration')

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index d72a9d0e..515ec16d 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1275,7 +1275,7 @@ namespace VC {
           IdentifierExpr v_prime_exp = new IdentifierExpr(v_prime.tok, v_prime);
           #endregion
           #region Create the assume command itself
-          AssumeCmd ac = new AssumeCmd(v.tok, TypedExprEq(v_prime_exp, pred_incarnation_exp));
+          AssumeCmd ac = new AssumeCmd(v.tok, TypedExprEq(v_prime_exp, pred_incarnation_exp, v_prime.Name.Contains("a##post##")));
           pred.Cmds.Add(ac);
           #endregion
           #endregion
@@ -1697,7 +1697,7 @@ namespace VC {
             }
           
             #region Create an assume command with the new variable
-            assumptions.Add(TypedExprEq(x_prime_exp, copies[i]));
+            assumptions.Add(TypedExprEq(x_prime_exp, copies[i], x_prime_exp.Decl != null && x_prime_exp.Decl.Name.Contains("a##post##")));
             #endregion
           }
         }
@@ -1815,10 +1815,15 @@ namespace VC {
       #endregion
     }
 
-    NAryExpr TypedExprEq(Expr e0, Expr e1) {
+    NAryExpr TypedExprEq(Expr e0, Expr e1, bool doNotResolveOverloading = false) {
       Contract.Requires(e0 != null);
       Contract.Requires(e1 != null);
       NAryExpr e = Expr.Eq(e0, e1);
+      var fun = e.Fun as IOverloadedAppliable;
+      if (fun != null)
+      {
+        fun.DoNotResolveOverloading = doNotResolveOverloading;
+      }
       e.Type = Bpl.Type.Bool;
       e.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
       return e;
-- 
cgit v1.2.3