diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-07-05 16:03:33 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-07-05 16:03:33 -0700 |
| commit | ca4a9b7b99dd6b6d43bb50a85b443e04ee821f81 (patch) | |
| tree | 2e3368daf3c031bef943eb568eae53bc894f316a /Source/Provers | |
| parent | 99d84bd265479e480e75f82de9917e9a4dc96b9b (diff) | |
Don't send (check-sat) after error limit is reached
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index c27f6a48..bc137492 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -346,8 +346,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(" ") + ")");
- SendThisVC("(assert " + expr + ")");
- SendThisVC("(check-sat)");
+ if (errorsLeft > 0) {
+ SendThisVC("(assert " + expr + ")");
+ SendThisVC("(check-sat)");
+ }
}
SendThisVC("(pop 1)");
|