check last result in (get-assignment); some context cleanup

1 files changed, 10 insertions, 5 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3d6f304b5..594efcc35 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -88,8 +88,7 @@ public:
   /**
    * Pre-process an Node.  This is expected to be highly-variable,
    * with a lot of "source-level configurability" to add multiple
-   * passes over the Node.  TODO: may need to specify a LEVEL of
-   * preprocessing (certain contexts need more/less ?).
+   * passes over the Node.
    */
   static Node preprocess(SmtEngine& smt, TNode n)
     throw(NoSuchFunctionException, AssertionException);
@@ -488,7 +487,8 @@ Expr SmtEngine::getValue(const Expr& e)
       "Cannot get value when produce-models options is off.";
     throw ModalException(msg);
   }
-  if(d_status.asSatisfiabilityResult() != Result::SAT ||
+  if(d_status.isNull() ||
+     d_status.asSatisfiabilityResult() != Result::SAT ||
      d_haveAdditions) {
     const char* msg =
       "Cannot get value unless immediately proceded by SAT/INVALID response.";
@@ -548,8 +548,13 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
       "produce-assignments option is off.";
     throw ModalException(msg);
   }
-  // TODO also check that the last query was sat/unknown, without intervening
-  // assertions
+  if(d_status.isNull() ||
+     d_status.asSatisfiabilityResult() != Result::SAT ||
+     d_haveAdditions) {
+    const char* msg =
+      "Cannot get value unless immediately proceded by SAT/INVALID response.";
+    throw ModalException(msg);
+  }
 
   NodeManagerScope nms(d_nodeManager);
   vector<SExpr> sexprs;