diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-23 15:44:50 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-23 15:44:50 -0500 |
| commit | a96fbfe33c05bea0b94d5387dda65c2ae343f66b (patch) | |
| tree | a3b1e28dc45f05ef218331217ed072e842d6dfd3 /src/theory/theory_engine.cpp | |
| parent | 4c2138a14c4abba2431bc8ba51359d3a565baf05 (diff) | |
Add notions of evaluated kinds in TheoryModel (#1947)
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 08d33fe6c..4d78482c5 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -232,7 +232,8 @@ void TheoryEngine::finishInit() { d_curr_model_builder = d_quantEngine->getModelBuilder(); d_curr_model = d_quantEngine->getModel(); } else { - d_curr_model = new theory::TheoryModel(d_userContext, "DefaultModel", true); + d_curr_model = new theory::TheoryModel( + d_userContext, "DefaultModel", options::assignFunctionValues()); d_aloc_curr_model = true; } //make the default builder, e.g. in the case that the quantifiers engine does not have a model builder |