Skip to content

Commit 2a86fb4

Browse files
committed
Bugfix: always print path exploration resume point
Before this commit, CBMC would occasionally print "Resuming from ''" because the source location that it was accessing was null.
1 parent e823538 commit 2a86fb4

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

src/goto-symex/symex_goto.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -169,7 +169,8 @@ void goto_symext::symex_goto(statet &state)
169169
goto_programt::const_targett tmp = new_state_pc;
170170
new_state_pc = state_pc;
171171
state_pc = tmp;
172-
log.debug() << "Resuming from '" << state_pc->code.source_location() << "'"
172+
173+
log.debug() << "Resuming from '" << state_pc->source_location << "'"
173174
<< log.eom;
174175
}
175176
else if(options.get_bool_option("paths"))

0 commit comments

Comments
 (0)