Merge pull request #7287 from thomasspriggs/tas/catch_smt

Fix printing of SMT data structures in failed unit tests

Author: thomasspriggs

regression/catch-framework/irep-printing/smt.desc

@@ -0,0 +1,13 @@
+CORE
+[smt_error_printing]
+
+Bool \=\= \(_ BitVec 8\)
+\(_ bv42 8\) \=\= false
+\(check\-sat\) \=\= \(set\-logic ALL\)
+^EXIT=0$
+^SIGNAL=0$
+--
+\{\?\}
+--
+Test that when unit tests fail on mismatching smt data structures, the ireps are
+pretty-printed and not printed as catch's default of {?}.

unit/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -244,3 +244,16 @@ TEST_CASE("SMT exists term to string conversion", "[core][smt2_incremental]")
       "(exists ((i (_ BitVec 8)) (j Bool)) (or (= i i) j))");
   }
 }
+
+// This test is expected to fail so that we can test the error printing of the
+// unit test framework for regressions. It is not included in the [core] or
+// default set of tests, so that the usual output is not polluted with
+// irrelevant error messages.
+TEST_CASE(
+  "Catch2 printing of SMT data structures for test failures.",
+  "[smt_error_printing]" XFAIL)
+{
+  CHECK(smt_bool_sortt{} == smt_bit_vector_sortt{8});
+  CHECK(smt_bit_vector_constant_termt{42, 8} == smt_bool_literal_termt{false});
+  CHECK(smt_check_sat_commandt{} == smt_set_logic_commandt{smt_logic_allt{}});
+}

unit/testing-utils/use_catch.h

@@ -42,4 +42,6 @@ Author: Michael Tautschnig
 class irept;
 std::ostream &operator<<(std::ostream &os, const irept &value);
 
+#include <solvers/smt2_incremental/smt_to_smt2_string.h>
+
 #endif // CPROVER_TESTING_UTILS_USE_CATCH_H