diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-12-28 19:24:35 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-12-28 19:24:35 -0800 |
| commit | c8b95a25e4e458aad19ef3891e7a09d3032d2ac0 (patch) | |
| tree | f55ff85eb6914f961458d80ad09992e7eab9b68c /src/theory | |
| parent | c0d75b9ead289143749bcd030e390e614d4658e5 (diff) | |
Add unit tests for side conditions for inequality for CBQI BV. (#1455)
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/quantifiers/bv_inverter.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index a970e3395..cdabaabb8 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -363,7 +363,7 @@ static Node getScBvUrem(bool pol, Node t) { Assert(k == BITVECTOR_UREM_TOTAL); - Assert(pol == false || idx == 1); + Assert(litk != EQUAL || pol == false || idx == 1); NodeManager* nm = NodeManager::currentNM(); |