Optimized the VC generation for assumption variables.

1 files changed, 2 insertions, 2 deletions

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)