From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 29 Dec 2017 04:27:58 +0000 (-0800)
Subject: Fix unit tests for ineq for CBQI BV. (#1456)
X-Git-Tag: cvc5-1.0.0~5402
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6375437da22d1397b251cc1fb9e6691f13c969f8;p=cvc5.git

Fix unit tests for ineq for CBQI BV. (#1456)
---

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)