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.

diff --git a/src/util/iand.h b/src/util/iand.h
index 117ab6f022cc4a3909b0c36df35bba38901a0e56..6c29c38b45405523a8842b0cc1d230321ee81492 100644 (file)
--- 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 68748d4a5cb23ee77f4a7ea5b8f78af343385797..e866d789c02bc02af928b6052e09ac85d0bc2e07 100644 (file)
--- 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 1b1fca2ac095d7590db408d9be7d5f6c47743198..42dfb1bfc0514cdb3d9b737c0b6af0cbd72bd9eb 100644 (file)
--- 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 766d696a18e60705500aa35e197d023a503530d5..d8ae8e4682387c2d935afa84f82427619c9a2066 100644 (file)
--- 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());