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/Core/AbsyExpr.cs | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

(limited to 'Source/Core/AbsyExpr.cs')

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) {
-- 
cgit v1.2.3