diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-09-30 19:41:36 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-30 12:41:36 -0500 |
| commit | 2bd861b27f6e340ea5f6739ac57bb6ffa61ffbfc (patch) | |
| tree | 0b5fae9aa5a4a3b70f6828955cc2cc8330d3b6d3 /src/theory/arith/theory_arith.cpp | |
| parent | 5ac936654df0f214e308a48116dcf6190d6255e2 (diff) | |
Remove too strict assertion to allow for approximate models (#5168)
This PR simply removes an assertion that would trigger whenever the arithmetic theory asserts a model that contains something else than a constant. This can be the case with witness terms.
In offline discussion we concluded that this discussion was overly strict. Note that these examples may still hit an error during model validation (Cannot run check-model on a model with approximate values.).
This PR also fixes a debug output I found during debugging.
Fixes #5113.
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index f16e0a297..d84f666be 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -158,7 +158,6 @@ bool TheoryArith::collectModelValues(TheoryModel* m, { // maps to constant of comparable type Assert(p.first.getType().isComparableTo(p.second.getType())); - Assert(p.second.isConst()); if (m->assertEquality(p.first, p.second, true)) { continue; |