Add notions of evaluated kinds in TheoryModel (#1947)

1 files changed, 8 insertions, 1 deletions

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index e88d1e3be..f91a413e3 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -930,7 +930,10 @@ bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m)
 
 bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m)
 {
-  assignFunctions(m);
+  if (m->areFunctionValuesEnabled())
+  {
+    assignFunctions(m);
+  }
   return true;
 }
 
@@ -1098,6 +1101,10 @@ struct sortTypeSize
 
 void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m)
 {
+  if (!options::assignFunctionValues())
+  {
+    return;
+  }
   Trace("model-builder") << "Assigning function values..." << std::endl;
   std::vector<Node> funcs_to_assign = m->getFunctionsToAssign();