Use explicit mechanism for skipping to the next assertion

4 files changed, 34 insertions, 13 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index f299af30..e327a3e8 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -258,7 +258,7 @@ namespace Microsoft.Boogie.SMTLib
       var globalResult = Outcome.Undetermined;

 

       while (errorsLeft-- > 0) {

-        var seenLabels = false;

+        string negLabel = null;

 

         result = GetResponse();

         if (globalResult == Outcome.Undetermined)

@@ -273,15 +273,19 @@ namespace Microsoft.Boogie.SMTLib
             if (resp == null || Process.IsPong(resp))

               break;

             if (resp.Name == ":labels" && resp.ArgCount >= 1) {

-              var labels = resp[0].Arguments.Select(a => a.Name.Replace("|", "").Replace("@", "").Replace("+", "")).ToList();

-              handler.OnModel(labels, null);

-              seenLabels = true;

+              var labels = resp[0].Arguments.Select(a => a.Name.Replace("|", "")).ToArray();

+              negLabel = labels.FirstOrDefault(l => l.StartsWith("@"));

+              var labelNums = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList();

+              handler.OnModel(labelNums, null);

+              if (negLabel == null)

+                HandleProverError("No negative label in: " + labels.Concat(" "));

             }

           }

         }

 

-        if (!seenLabels) break;

-        SendThisVC("(next-sat)");

+        if (negLabel == null) break;

+        SendThisVC("(assert " + SMTLibNamer.QuoteId(SMTLibNamer.BlockedLabel(negLabel)) + ")");

+        SendThisVC("(check-sat)");

       }

 

       SendThisVC("(pop 1)");

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 7df58b9e..8389ed50 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -477,11 +477,18 @@ namespace Microsoft.Boogie.SMTLib
         if (ExprLineariser.ProverOptions.UseLabels) {

           // Z3 extension

           wr.Write("({0} {1} ", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label));

-          ExprLineariser.Linearise(node[0], options);

-          wr.Write(")");

-        } else {

-          ExprLineariser.Linearise(node[0], options);

         }

+

+        if (!op.pos)

+          wr.Write("(or {0} ", SMTLibNamer.QuoteId(SMTLibNamer.BlockedLabel(op.label)));

+            

+        ExprLineariser.Linearise(node[0], options);

+

+        if (!op.pos) wr.Write(")");

+

+        if (ExprLineariser.ProverOptions.UseLabels)

+          wr.Write(")");

+

         return true;

       }

 

diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
index 2f8e86c8..80de8e3f 100644
--- a/Source/Provers/SMTLib/SMTLibNamer.cs
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -87,6 +87,11 @@ namespace Microsoft.Boogie.SMTLib
       return s;

     }

 

+    public static string BlockedLabel(string s)

+    {

+      return "%block%" + s;

+    }

+

     public static string QuoteId(string s)

     {

       return AddQuotes(NonKeyword(s));

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 05c0ed9e..a4af7f40 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -52,10 +52,10 @@ void ObjectInvariant()
     private readonly IDictionary<VCExprVar/*!*/, bool>/*!*/ KnownVariables =

       new Dictionary<VCExprVar/*!*/, bool> ();

 

-

     private readonly Dictionary<Type/*!*/, bool>/*!*/ KnownTypes = new Dictionary<Type, bool>();

     private readonly Dictionary<string/*!*/, bool>/*!*/ KnownStoreFunctions = new Dictionary<string, bool>();

     private readonly Dictionary<string/*!*/, bool>/*!*/ KnownSelectFunctions = new Dictionary<string, bool>();

+    private readonly HashSet<string> KnownLBLNEG = new HashSet<string>();

 

 

     public List<string/*!>!*/> AllDeclarations { get {

@@ -118,6 +118,13 @@ void ObjectInvariant()
           string decl = "(declare-fun " + printedName + " (" + argTypes + ") " + TypeToStringReg(f.OutParams[0].TypedIdent.Type) + ")";

           AddDeclaration(decl);

           KnownFunctions.Add(f, true);

+        } else {

+          var lab = node.Op as VCExprLabelOp;

+          if (lab != null && !lab.pos && !KnownLBLNEG.Contains(lab.label)) {

+            KnownLBLNEG.Add(lab.label);

+            var name = SMTLibNamer.QuoteId(SMTLibNamer.BlockedLabel(lab.label));

+            AddDeclaration("(declare-fun " + name + " () Bool)");

+          }

         }

       }

 

@@ -139,8 +146,6 @@ void ObjectInvariant()
       return base.Visit(node, arg);

     }

 

-

-

     public override bool Visit(VCExprQuantifier node, bool arg)

     {

       Contract.Requires(node != null);