Improve support for identifying unnecessary assumes.

2 files changed, 7 insertions, 2 deletions

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index ae4d158a..7bda0022 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -453,6 +453,10 @@ namespace Microsoft.Boogie {
       Undetermined,
       Bounded
     }
+
+    public readonly ISet<VCExprVar> NamedAssumes = new HashSet<VCExprVar>();
+    public ISet<string> UsedNamedAssumes { get; protected set; }
+
     public class ErrorHandler {
       // Used in CheckOutcomeCore
       public virtual int StartingProcId()
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index d18c544a..cad5914b 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -193,9 +193,10 @@ namespace VC {
         var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);
         
         var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id");
-        if (CommandLineOptions.Clo.PrintNecessaryAssumes && aid != null)
+        if (aid != null)
         {
-          var v = gen.Variable("assume$$" + aid, Microsoft.Boogie.Type.Bool);
+          var isTry = QKeyValue.FindBoolAttribute(ac.Attributes, "try");
+          var v = gen.Variable((isTry ? "try$$" : "assume$$") + aid, Microsoft.Boogie.Type.Bool);
           expr = gen.Function(VCExpressionGenerator.NamedAssumeOp, v, gen.ImpliesSimp(v, expr));
         }
         var soft = QKeyValue.FindBoolAttribute(ac.Attributes, "soft");