Filter out duplicate source locations in witness

Author: peterschrammel

src/goto-programs/graphml_witness.cpp

@@ -6,8 +6,6 @@ Author: Daniel Kroening
 
 \*******************************************************************/
 
-#include <iostream>
-
 #include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/config.h>
@@ -179,6 +177,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
   // step numbers start at 1
   std::vector<std::size_t> step_to_node(goto_trace.steps.size()+1, 0);
 
+  goto_tracet::stepst::const_iterator prev_it=goto_trace.steps.end();
   for(goto_tracet::stepst::const_iterator
       it=goto_trace.steps.begin();
       it!=goto_trace.steps.end();
@@ -188,6 +187,11 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
 
     if(it->hidden ||
        (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
+       // we filter out steps with the same source location
+       // TODO: if these are assignments we should accumulate them into
+       //       a single edge
+       (prev_it!=goto_trace.steps.end() &&
+        prev_it->pc->source_location==it->pc->source_location) ||
        (it->is_goto() && it->pc->guard.is_true()) ||
        source_location.is_nil() ||
        source_location.get_file().empty() ||
@@ -212,6 +216,8 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
       continue;
     }
 
+    prev_it=it;
+
     const graphmlt::node_indext node=graphml.add_node();
     graphml[node].node_name=
       i2string(it->pc->location_number)+"."+i2string(it->step_nr);