From 994fdafa5e496c007e78274093f7b02fa2e8dd06 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Fri, 30 Jan 2015 12:52:21 +0100
Subject: Minor change to the encoding of partially verified assertions as VC

---
 Source/VCGeneration/Wlp.cs | 55 +++++++++++++++++++++++++++-------------------
 1 file changed, 32 insertions(+), 23 deletions(-)

(limited to 'Source/VCGeneration')

diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index cd735501..45e511f0 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -26,13 +26,6 @@ namespace VC {
     public int AssertionCount;  // counts the number of assertions for which Wlp has been computed
     public bool isPositiveContext;
 
-    int letBindingCount;
-    public string FreshLetBindingName()
-    {
-      var c = System.Threading.Interlocked.Increment(ref letBindingCount);
-      return string.Format("v##let##{0}", c);
-    }
-
     public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt, bool isPositiveContext = true)
     {
       Contract.Requires(ctxt != null);
@@ -104,41 +97,57 @@ namespace VC {
       Contract.Assert(gen != null);
       if (cmd is AssertCmd) {
         AssertCmd ac = (AssertCmd)cmd;
-        ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext;
+
+        var isFullyVerified = false;
+        if (ac.VerifiedUnder != null)
+        {
+          var litExpr = ac.VerifiedUnder as LiteralExpr;
+          isFullyVerified = litExpr != null && litExpr.IsTrue;
+        }
+
+        if (!isFullyVerified)
+        {
+          ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext;
+        }
+
         VCExpr C = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);
+
         VCExpr VU = null;
-        if (ac.VerifiedUnder != null)
+        if (!isFullyVerified)
         {
-          VU = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.VerifiedUnder);
+          if (ac.VerifiedUnder != null)
+          {
+            VU = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.VerifiedUnder);
+          }
+          ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext;
         }
-        ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext; 
 
         VCExpr R = null;
         if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
           R = gen.Implies(C, N);
         } else {
-          int id = ac.UniqueId;
-          if (ctxt.Label2absy != null) {
-            ctxt.Label2absy[id] = ac;
-          }
-
           var subsumption = Subsumption(ac);
           if (subsumption == CommandLineOptions.SubsumptionOption.Always
               || (subsumption == CommandLineOptions.SubsumptionOption.NotForQuantifiers && !(C is VCExprQuantifier)))
           {
-            N = gen.ImpliesSimp(C, N);
+            N = gen.ImpliesSimp(C, N, false);
           }
 
-          if (VU != null)
+          if (isFullyVerified)
+          {
+            return N;
+          }
+          else if (VU != null)
           {
-            var litExpr = ac.VerifiedUnder as LiteralExpr;
-            if (litExpr != null && litExpr.IsTrue)
-            {
-              return N;
-            }
             C = gen.OrSimp(VU, C);
           }
 
+          int id = ac.UniqueId;
+          if (ctxt.Label2absy != null)
+          {
+            ctxt.Label2absy[id] = ac;
+          }
+
           ctxt.AssertionCount++;
 
           if (ctxt.ControlFlowVariableExpr == null) {
-- 
cgit v1.2.3