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

1 files changed, 21 insertions, 0 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) {