diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-30 03:32:47 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-30 01:32:47 -0800 |
commit | 13ef9140d1ba6740ccb2c1f29bd2d243de6872c2 (patch) | |
tree | 1626d5979182f94f12c9fc28a4a9046edb5d1304 /src/theory/theory_model_builder.cpp | |
parent | e3361a428a1b24369d782120de1f050874a8ac44 (diff) |
Do not debug check model for models with approximations (#3673)
We don't run check-model for models with approximate values, however we were still running the internal debugCheckModel method, which leads to assertion failures. This disables this check.
Fixes #3652.
Diffstat (limited to 'src/theory/theory_model_builder.cpp')
-rw-r--r-- | src/theory/theory_model_builder.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 11758f1e9..02dded8b3 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -1127,6 +1127,11 @@ void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm) { #ifdef CVC4_ASSERTIONS Assert(tm->isBuilt()); + if (tm->hasApproximations()) + { + // models with approximations may fail the assertions below + return; + } eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); std::map<Node, Node>::iterator itMap; // Check that every term evaluates to its representative in the model |