From 6375437da22d1397b251cc1fb9e6691f13c969f8 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 28 Dec 2017 20:27:58 -0800 Subject: [PATCH] Fix unit tests for ineq for CBQI BV. (#1456) --- test/unit/theory/theory_quantifiers_bv_inverter_white.h | 6 +++--- 1 file 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) -- 2.30.2