diff options
Diffstat (limited to 'src/theory/theory_model_builder.cpp')
-rw-r--r-- | src/theory/theory_model_builder.cpp | 24 |
1 files changed, 19 insertions, 5 deletions
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index bcc4f7eaf..a9742b2ba 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -808,16 +808,30 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) { return false; } - else + + tm->d_modelBuiltSuccess = true; + return true; +} + +void TheoryEngineModelBuilder::postProcessModel(bool incomplete, Model* m) +{ + // if we are incomplete, there is no guarantee on the model. + // thus, we do not check the model here. (related to #1693). + if (incomplete) { - tm->d_modelBuiltSuccess = true; - return true; + return; + } + TheoryModel* tm = static_cast<TheoryModel*>(m); + Assert(tm != nullptr); + // debug-check the model if the checkModels() is enabled. + if (options::checkModels()) + { + debugCheckModel(tm); } } -void TheoryEngineModelBuilder::debugCheckModel(Model* m) +void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm) { - TheoryModel* tm = (TheoryModel*)m; #ifdef CVC4_ASSERTIONS Assert(tm->isBuilt()); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); |