From 84670125bef08609d4c447c27f245fef530ebcd2 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Wed, 29 May 2013 17:45:48 -0700
Subject: Minor change to prevent prover errors during trace extraction

---
 Source/Provers/SMTLib/ProverInterface.cs | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'Source/Provers/SMTLib/ProverInterface.cs')

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index d91ca010..7cd3b3cd 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -790,7 +790,7 @@ namespace Microsoft.Boogie.SMTLib
             handler.OnModel(xlabels, model);
           }
 
-          if (labels == null || errorsLeft == 0) break;
+          if (labels == null || !labels.Any() || errorsLeft == 0) break;
 
           if (CommandLineOptions.Clo.UseLabels) {
             var negLabels = labels.Where(l => l.StartsWith("@")).ToArray();
@@ -800,6 +800,10 @@ namespace Microsoft.Boogie.SMTLib
               posLabels = Enumerable.Empty<string>();
             var conjuncts = posLabels.Select(s => "(not " + lbl(s) + ")").Concat(negLabels.Select(lbl)).ToArray();
             var expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")");
+            if (!conjuncts.Any())
+            {
+              expr = "false";
+            }
             SendThisVC("(assert " + expr + ")");
             SendThisVC("(check-sat)");
           }
-- 
cgit v1.2.3