Skip to content

Commit 7a0da55

Browse files
committed
Improve error printing in smt2 decision procedure unit test
In order to improve the chances of being able to see what is wrong when/if the tests fail.
1 parent 91da8ba commit 7a0da55

File tree

1 file changed

+6
-0
lines changed

1 file changed

+6
-0
lines changed

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,12 @@
1414
#include <util/namespace.h>
1515
#include <util/symbol_table.h>
1616

17+
// Used by catch framework for printing in the case of test failures. This
18+
// means that we get error messages showing the smt formula expressed as SMT2
19+
// strings instead of `{?}` being printed. It works because catch uses the
20+
// appropriate overload of `operator<<` where it exists.
21+
#include <solvers/smt2_incremental/smt_to_smt2_string.h>
22+
1723
class smt_mock_solver_processt : public smt_base_solver_processt
1824
{
1925
public:

0 commit comments

Comments
 (0)