summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/smt_engine.cpp9
1 files changed, 5 insertions, 4 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4cb76eda6..4a7c9def3 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4641,11 +4641,12 @@ void SmtEngine::checkUnsatCore() {
}
Notice() << "SmtEngine::checkUnsatCore(): result is " << r << endl;
if(r.asSatisfiabilityResult().isUnknown()) {
- InternalError()
- << "SmtEngine::checkUnsatCore(): could not check core result unknown.";
+ Warning()
+ << "SmtEngine::checkUnsatCore(): could not check core result unknown."
+ << std::endl;
}
-
- if(r.asSatisfiabilityResult().isSat()) {
+ else if (r.asSatisfiabilityResult().isSat())
+ {
InternalError()
<< "SmtEngine::checkUnsatCore(): produced core was satisfiable.";
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback