From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 27 Jul 2021 06:36:18 +0000 (-0500)
Subject: Minor changes from proof-new (#6937)
X-Git-Tag: cvc5-1.0.0~1447
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a9fcf2d394e3d36c6058d480e350cda350935f70;p=cvc5.git

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 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());