Skip to content

Commit eb5b1c4

Browse files
committed
Remove invariant on full_lhs_value in printing goto_tracet
This invariant in the printing is preventing other, otherwise usefull output from being printed, in the case where a goto trace has been produced which contains a `full_lhs_value` set to `nil` in an assignment step.
1 parent f179ca8 commit eb5b1c4

File tree

1 file changed

+0
-3
lines changed

1 file changed

+0
-3
lines changed

src/goto-programs/json_goto_trace.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -132,9 +132,6 @@ void convert_decl(
132132
}
133133
else
134134
{
135-
DATA_INVARIANT(
136-
step.full_lhs_value.is_not_nil(),
137-
"full_lhs_value in assignment must not be nil");
138135
full_lhs_value = json(step.full_lhs_value, ns, ID_unknown);
139136
}
140137

0 commit comments

Comments
 (0)