summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/ProverInterface.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Provers/SMTLib/ProverInterface.cs')
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs6
1 files changed, 5 insertions, 1 deletions
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)");
}