Skip to content

Commit cedc94e

Browse files
committed
Do not output right-hand sides of assignments in symex debug output
The right-hand side may be a large expression and clutters the output.
1 parent 36e4d6f commit cedc94e

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/goto-symex/symex_target_equation.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -915,13 +915,13 @@ void symex_target_equationt::SSA_stept::output(std::ostream &out) const
915915
UNREACHABLE;
916916
}
917917

918-
if(is_assert() || is_assume() || is_assignment() || is_constraint())
918+
if(is_assert() || is_assume() || is_constraint())
919919
out << format(cond_expr) << '\n';
920920

921921
if(is_assert() || is_constraint())
922922
out << comment << '\n';
923923

924-
if(is_shared_read() || is_shared_write())
924+
if(is_shared_read() || is_shared_write() || is_assignment())
925925
out << format(ssa_lhs) << '\n';
926926

927927
out << "Guard: " << format(guard) << '\n';

0 commit comments

Comments
 (0)