diff options
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) |