2 files changed, 5 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6e8cc9b5d..cedd866f9 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1888,7 +1888,7 @@ Expr SmtEngine::getValue(const Expr& e)
       "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response.";
     throw ModalException(msg);
   }
-  if(type.isKind() || type.isSortConstructor()) {
+  if(type.isSort() || type.isSortConstructor()) {
     const char* msg =
       "Cannot get value of a sort.";
     throw ModalException(msg);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index cbb97f9f7..0214cddd3 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -559,7 +559,10 @@ public:
    */
   SExpr getStatistic(std::string name) const throw();
 
-  Result getStatusOfLastCommand() const {
+  /**
+   * Returns the most recent result of checkSat/query or (set-info :status).
+   */
+  Result getStatusOfLastCommand() const throw() {
     return d_status;
   }