From 575d226a8e15efc111bfaf57f188261e12f7ef95 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Sun, 7 Dec 2014 15:58:48 +0100
Subject: Optimized the VC generation for assumption variables.

---
 Source/Core/Absy.cs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Source/Core')

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index a5955c7a..b491f872 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -3298,12 +3298,12 @@ namespace Microsoft.Boogie {
 
     public List<LocalVariable> RelevantInjectedAssumptionVariables(Dictionary<Variable, Expr> incarnationMap)
     {
-      return InjectedAssumptionVariables.Where(v => incarnationMap.ContainsKey(v)).ToList();
+      return InjectedAssumptionVariables.Where(v => { Expr e; if (incarnationMap.TryGetValue(v, out e)) { var le = e as LiteralExpr; return le == null || !le.IsTrue; } else { return false; } }).ToList();
     }
 
     public List<LocalVariable> RelevantDoomedInjectedAssumptionVariables(Dictionary<Variable, Expr> incarnationMap)
     {
-      return DoomedInjectedAssumptionVariables.Where(v => incarnationMap.ContainsKey(v)).ToList();
+      return DoomedInjectedAssumptionVariables.Where(v => { Expr e; if (incarnationMap.TryGetValue(v, out e)) { var le = e as LiteralExpr; return le == null || !le.IsTrue; } else { return false; } }).ToList();
     }
 
     public Expr ConjunctionOfInjectedAssumptionVariables(Dictionary<Variable, Expr> incarnationMap, out bool isTrue)
-- 
cgit v1.2.3