diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-02-07 22:31:08 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-08 00:31:08 -0600 |
commit | 618282e081393683c3d986726b8601ba33310e79 (patch) | |
tree | 9a7f3a91f9d9ca28c66e2f1514e8eb6d7632a264 /src | |
parent | 3f9b6b57255d38fa9bee6b66dae3b8932703135a (diff) |
Make "unknown" non-critical for unsat cores check (#3728)
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 9 |
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."; } |