Made it produce slightly different passive commands for assignments to assumption variables.

2 files changed, 29 insertions, 3 deletions

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 75a5741a..1b5cc3d4 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1197,6 +1197,7 @@ namespace Microsoft.Boogie {
   [ContractClass(typeof(IOverloadedAppliableContracts))]

   public interface IOverloadedAppliable {

     void ResolveOverloading(NAryExpr/*!*/ expr);

+    bool DoNotResolveOverloading { get; set; }

   }

   [ContractClassFor(typeof(IOverloadedAppliable))]

   public abstract class IOverloadedAppliableContracts : IOverloadedAppliable {

@@ -1208,6 +1209,18 @@ namespace Microsoft.Boogie {
       throw new NotImplementedException();

     }

 

+    public bool DoNotResolveOverloading

+    {

+      get

+      {

+        throw new NotImplementedException();

+      }

+      set

+      {

+        throw new NotImplementedException();

+      }

+    }

+

     #endregion

   }

 

@@ -1383,6 +1396,8 @@ namespace Microsoft.Boogie {
       Contract.Invariant(tok != null);

     }

 

+    public bool DoNotResolveOverloading { get; set; }

+

     public enum Opcode {

       Add,

       Sub,

@@ -1740,6 +1755,12 @@ namespace Microsoft.Boogie {
 

     public void ResolveOverloading(NAryExpr expr) {

       //Contract.Requires(expr != null);

+

+      if (DoNotResolveOverloading)

+      {

+        return;

+      }

+

       Expr arg0 = cce.NonNull(expr.Args[0]);

       Expr arg1 = cce.NonNull(expr.Args[1]);

       switch (op) {

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;