diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-12-28 20:27:58 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-12-28 20:27:58 -0800 |
| commit | 6375437da22d1397b251cc1fb9e6691f13c969f8 (patch) | |
| tree | 107cd6b7b35e3c6644b997dfb0a52c6fe0abc9fe /test/unit/theory | |
| parent | c8b95a25e4e458aad19ef3891e7a09d3032d2ac0 (diff) | |
Fix unit tests for ineq for CBQI BV. (#1456)
Diffstat (limited to 'test/unit/theory')
| -rw-r--r-- | test/unit/theory/theory_quantifiers_bv_inverter_white.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h index 48df04845..e1d950050 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h @@ -103,9 +103,9 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite || ksc == IMPLIES); Node scl = ksc == IMPLIES ? sc[0] : bv::utils::mkTrue(); Node body = idx == 0 - ? d_nm->mkNode(pol ? EQUAL : DISTINCT, d_nm->mkNode(k, d_x, d_s), d_t) - : d_nm->mkNode(pol ? EQUAL : DISTINCT, d_nm->mkNode(k, d_s, d_x), d_t); - Node scr = d_nm->mkNode(EXISTS, d_bvarlist, body); + ? d_nm->mkNode(litk, d_nm->mkNode(k, d_x, d_s), d_t) + : d_nm->mkNode(litk, d_nm->mkNode(k, d_s, d_x), d_t); + Node scr = d_nm->mkNode(EXISTS, d_bvarlist, pol ? body : body.notNode()); Expr a = d_nm->mkNode(DISTINCT, scl, scr).toExpr(); Result res = d_smt->checkSat(a); if (res.d_sat == Result::SAT) |