Skip to content

Commit 3d39a6f

Browse files
committed
goto-symex: Print (at debug level) the current assertion being converted
For other step types this had already been done in "Print (at debug level) the current SSA step being converted."
1 parent 072b592 commit 3d39a6f

File tree

1 file changed

+8
-0
lines changed

1 file changed

+8
-0
lines changed

src/goto-symex/symex_target_equation.cpp

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -623,6 +623,14 @@ void symex_target_equationt::convert_assertions(
623623
{
624624
if(step.is_assert())
625625
{
626+
prop_conv.conditional_output(
627+
prop_conv.debug(),
628+
[&step](messaget::mstreamt &mstream) {
629+
std::ostringstream oss;
630+
step.output(oss);
631+
mstream << oss.str() << messaget::eom;
632+
});
633+
626634
implies_exprt implication(
627635
assumption,
628636
step.cond_expr);

0 commit comments

Comments
 (0)