diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-27 06:47:07 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-27 06:47:07 -0500 |
| commit | c74d62444151a777612af114d50dea9233f64273 (patch) | |
| tree | 4f8a92634f5f40b50f944b805c4dd1780aacde66 | |
| parent | dd86535c0a7dba3a7a3db2453eaf3b5c7abaaacc (diff) | |
| parent | a9fcf2d394e3d36c6058d480e350cda350935f70 (diff) | |
Merge branch 'master' into fix6639fix6639
| -rw-r--r-- | src/util/iand.h | 2 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/stoi-400million.smt2 | 2 | ||||
| -rw-r--r-- | 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()); |