Add notions of evaluated kinds in TheoryModel (#1947)

1 files changed, 12 insertions, 0 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 114527334..9d4462210 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1313,6 +1313,11 @@ void SmtEngine::setDefaults() {
     {
       options::cbqiMidpoint.set(true);
     }
+    // do not assign function values (optimization)
+    if (!options::assignFunctionValues.wasSetByUser())
+    {
+      options::assignFunctionValues.set(false);
+    }
   }
   else
   {
@@ -5189,6 +5194,13 @@ Model* SmtEngine::getModel() {
     Dump("benchmark") << GetModelCommand();
   }
 
+  if (!options::assignFunctionValues())
+  {
+    const char* msg =
+        "Cannot get the model when --assign-function-values is false.";
+    throw RecoverableModalException(msg);
+  }
+
   if(d_status.isNull() ||
      d_status.asSatisfiabilityResult() == Result::UNSAT ||
      d_problemExtended) {