diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-04 15:18:12 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-09-04 15:18:12 -0500 |
commit | a635120676d265b27fa7c49d86d16a3e6d96174e (patch) | |
tree | 978e5e4c8a688fde4a5b152937caea864bedba53 /src/theory/theory_engine.cpp | |
parent | d367c9f9b299a15fb970d62df04d3df22b7ca08d (diff) |
Minor improvements to theory model builder interface. (#2408)
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d75f7843d..41ab45170 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -636,17 +636,12 @@ void TheoryEngine::check(Theory::Effort effort) { AlwaysAssert(d_curr_model->isBuiltSuccess()); if (options::produceModels()) { - // if we are incomplete, there is no guarantee on the model. - // thus, we do not check the model here. (related to #1693) - // we also don't debug-check the model if the checkModels() - // is not enabled. - if (!d_incomplete && options::checkModels()) - { - d_curr_model_builder->debugCheckModel(d_curr_model); - } // Do post-processing of model from the theories (used for THEORY_SEP // to construct heap model) postProcessModel(d_curr_model); + // also call the model builder's post-process model + d_curr_model_builder->postProcessModel(d_incomplete.get(), + d_curr_model); } } } |