From a9fcf2d394e3d36c6058d480e350cda350935f70 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 27 Jul 2021 01:36:18 -0500 Subject: Minor changes from proof-new (#6937) Note the change to the unit test makes it so the test is not dependent on Node ID order. --- src/util/iand.h | 2 +- test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 | 1 - test/regress/regress1/strings/stoi-400million.smt2 | 2 +- test/unit/theory/theory_black.cpp | 3 +-- 4 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/util/iand.h b/src/util/iand.h index 117ab6f02..6c29c38b4 100644 --- a/src/util/iand.h +++ b/src/util/iand.h @@ -39,7 +39,7 @@ struct IntAnd inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia); inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia) { - return os << "[" << ia.d_size << "]"; + return os << "(_ iand " << ia.d_size << ")"; } } // namespace cvc5 diff --git a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 index 68748d4a5..e866d789c 100644 --- a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 +++ b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-unsat-cores --no-produce-proofs (set-logic AUFLIRA) (set-info :source | Example extracted from Peter Baumgartner's talk at CADE-21: Logical Engineering with Instance-Based Methods. diff --git a/test/regress/regress1/strings/stoi-400million.smt2 b/test/regress/regress1/strings/stoi-400million.smt2 index 1b1fca2ac..42dfb1bfc 100644 --- a/test/regress/regress1/strings/stoi-400million.smt2 +++ b/test/regress/regress1/strings/stoi-400million.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --strings-exp --no-produce-proofs --no-jh-rlv-order +; COMMAND-LINE: --strings-exp --no-jh-rlv-order ; EXPECT: sat (set-info :smt-lib-version 2.6) (set-logic ALL) diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp index 766d696a1..d8ae8e468 100644 --- a/test/unit/theory/theory_black.cpp +++ b/test/unit/theory/theory_black.cpp @@ -53,13 +53,12 @@ TEST_F(TestTheoryBlack, array_const) arr = d_nodeManager->mkNode(STORE, storeAll, zero, one); ASSERT_TRUE(arr.isConst()); Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); - ASSERT_FALSE(arr2.isConst()); arr2 = Rewriter::rewrite(arr2); ASSERT_TRUE(arr2.isConst()); arr2 = d_nodeManager->mkNode(STORE, arr, one, one); + arr2 = Rewriter::rewrite(arr2); ASSERT_TRUE(arr2.isConst()); arr2 = d_nodeManager->mkNode(STORE, arr, zero, one); - ASSERT_FALSE(arr2.isConst()); arr2 = Rewriter::rewrite(arr2); ASSERT_TRUE(arr2.isConst()); -- cgit v1.2.3