diff options
Diffstat (limited to 'test')
| -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 |
3 files changed, 2 insertions, 4 deletions
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()); |