Finish off SEXPR kind work.

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 0 insertions, 5 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ad72e0737..2db746c0a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1888,11 +1888,6 @@ Expr SmtEngine::getValue(const Expr& e)
       "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response.";
     throw ModalException(msg);
   }
-  if(type.isSort() || type.isSortConstructor()) {
-    const char* msg =
-      "Cannot get value of a sort.";
-    throw ModalException(msg);
-  }
 
   // do not need to apply preprocessing substitutions (should be recorded in model already)