Skip to content

Commit e545668

Browse files
Filter out duplicate source locations in witness
1 parent 1ebc80e commit e545668

File tree

1 file changed

+8
-1
lines changed

1 file changed

+8
-1
lines changed

src/goto-programs/graphml_witness.cpp

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -151,16 +151,21 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
151151
// step numbers start at 1
152152
std::vector<std::size_t> step_to_node(goto_trace.steps.size()+1, 0);
153153

154+
goto_tracet::stepst::const_iterator prev_it=goto_trace.steps.end();
154155
for(goto_tracet::stepst::const_iterator
155156
it=goto_trace.steps.begin();
156157
it!=goto_trace.steps.end();
157-
it++)
158+
it++) //we cannot replace this by a ranged for
158159
{
159160
const source_locationt &source_location=it->pc->source_location;
160161

161162
if(it->hidden ||
162163
(!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
164+
(prev_it!=goto_trace.steps.end() &&
165+
prev_it->pc->source_location==it->pc->source_location) ||
166+
#if 0
163167
(it->is_goto() && it->pc->guard.is_true()) ||
168+
#endif
164169
source_location.is_nil() ||
165170
source_location.get_file().empty() ||
166171
source_location.get_file()=="<built-in-additions>" ||
@@ -184,6 +189,8 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
184189
continue;
185190
}
186191

192+
prev_it=it;
193+
187194
const graphmlt::node_indext node=graphml.add_node();
188195
graphml[node].node_name=
189196
i2string(it->pc->location_number)+"."+i2string(it->step_nr);

0 commit comments

Comments
 (0)