diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 17:40:56 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 17:41:03 -0500 |
commit | 54d24c786d6a843cc72dfb5e377603349ea5e420 (patch) | |
tree | 09c68ea567da6ab079cdaac8a23876121dc2fc8d /src | |
parent | c24193a66e81f08cca82cb834fbd21ef630e1bcb (diff) |
Do not exit when value/model/unsat-core/proof is requested at wrong time, for bug 831.
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 20 |
1 files changed, 15 insertions, 5 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6960c4684..f6b17e4cb 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4775,7 +4775,9 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin d_problemExtended) { const char* msg = "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response."; - throw ModalException(msg); + //throw ModalException(msg); + Warning() << CommandFailure(msg); + return ex; } // Substitute out any abstract values in ex. @@ -4884,7 +4886,9 @@ CVC4::SExpr SmtEngine::getAssignment() { const char* msg = "Cannot get the current assignment unless immediately " "preceded by SAT/INVALID or UNKNOWN response."; - throw ModalException(msg); + //throw ModalException(msg); + Warning() << CommandFailure(msg); + return SExpr(vector<SExpr>()); } if(d_assignments == NULL) { @@ -4979,7 +4983,9 @@ Model* SmtEngine::getModel() { const char* msg = "Cannot get the current model unless immediately " "preceded by SAT/INVALID or UNKNOWN response."; - throw ModalException(msg); + //throw ModalException(msg); + Warning() << CommandFailure(msg); + return NULL; } if(!options::produceModels()) { const char* msg = @@ -5239,7 +5245,9 @@ UnsatCore SmtEngine::getUnsatCore() { if(d_status.isNull() || d_status.asSatisfiabilityResult() != Result::UNSAT || d_problemExtended) { - throw ModalException("Cannot get an unsat core unless immediately preceded by UNSAT/VALID response."); + //throw ModalException("Cannot get an unsat core unless immediately preceded by UNSAT/VALID response."); + Warning() << CommandFailure("Cannot get an unsat core unless immediately preceded by UNSAT/VALID response."); + return UnsatCore(); } d_proofManager->traceUnsatCore();// just to trigger core creation @@ -5263,7 +5271,9 @@ Proof* SmtEngine::getProof() { if(d_status.isNull() || d_status.asSatisfiabilityResult() != Result::UNSAT || d_problemExtended) { - throw ModalException("Cannot get a proof unless immediately preceded by UNSAT/VALID response."); + //throw ModalException("Cannot get a proof unless immediately preceded by UNSAT/VALID response."); + Warning() << CommandFailure("Cannot get a proof unless immediately preceded by UNSAT/VALID response."); + return NULL; } return ProofManager::getProof(this); |