From 06055fdd22eeb9015d215e71996e4714c183ef19 Mon Sep 17 00:00:00 2001
From: Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>
Date: Wed, 30 Jan 2013 12:43:15 -0800
Subject: handling old() in stable assertions bug fix in linear

---
 Source/Core/LinearSets.cs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

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

diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index ffbd4e31..4edbfeed 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -480,11 +480,15 @@ namespace Microsoft.Boogie
                 lhsVars.Add(v);
                 domainNames.Add(varToDomainName[v]);
             }
-            foreach (Variable v in lhsVars.Except(rhsVars))
+            foreach (Variable v in lhsVars.Union(rhsVars))
             {
                 Drain(newCmds, v, varToDomainName[v]);
             }
             newCmds.Add(callCmd);
+            foreach (string domainName in domainNames)
+            {
+                newCmds.Add(new AssumeCmd(Token.NoToken, DisjointnessExpr(domainName, domainNameToScope[domainName])));
+            } 
             IdentifierExprSeq havocExprs = new IdentifierExprSeq();
             foreach (Variable v in rhsVars.Except(lhsVars))
             {
@@ -494,10 +498,6 @@ namespace Microsoft.Boogie
             {
                 TransformHavocCmd(newCmds, new HavocCmd(Token.NoToken, havocExprs), copies, domainNameToScope);
             }
-            foreach (string domainName in domainNames)
-            {
-                newCmds.Add(new AssumeCmd(Token.NoToken, DisjointnessExpr(domainName, domainNameToScope[domainName])));
-            }
         }
 
         void TransformAssignCmd(CmdSeq newCmds, AssignCmd assignCmd, Dictionary<Variable, LocalVariable> copies, Dictionary<string, HashSet<Variable>> domainNameToScope)
-- 
cgit v1.2.3