Do not exit when value/model/unsat-core/proof is requested at wrong time, for bug 831.

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);