Get_all_property_ids should only return failed properties

Passed properties on traces are less interesting.

Author: peterschrammel

src/cbmc/c_test_input_generator.cpp

@@ -71,7 +71,7 @@ json_objectt test_inputst::to_json(
   }
 
   json_arrayt goal_refs;
-  for(const auto &goal_id : goto_trace.get_all_property_ids())
+  for(const auto &goal_id : goto_trace.get_failed_property_ids())
   {
     goal_refs.push_back(json_stringt(goal_id));
   }
@@ -105,7 +105,7 @@ xmlt test_inputst::to_xml(
     }
   }
 
-  for(const auto &goal_id : goto_trace.get_all_property_ids())
+  for(const auto &goal_id : goto_trace.get_failed_property_ids())
   {
     xmlt &xml_goal = xml_result.new_element("goal");
     xml_goal.set_attribute("id", id2string(goal_id));

src/goto-checker/goto_trace_storage.cpp

@@ -28,7 +28,7 @@ const goto_tracet &goto_trace_storaget::insert(goto_tracet &&trace)
 const goto_tracet &goto_trace_storaget::insert_all(goto_tracet &&trace)
 {
   traces.push_back(std::move(trace));
-  const auto &all_property_ids = traces.back().get_all_property_ids();
+  const auto &all_property_ids = traces.back().get_failed_property_ids();
   DATA_INVARIANT(
     !all_property_ids.empty(), "a trace must violate at least one assertion");
   for(const auto &property_id : all_property_ids)

src/goto-programs/goto_trace.cpp

@@ -773,13 +773,13 @@ void show_goto_trace(
 
 const trace_optionst trace_optionst::default_options = trace_optionst();
 
-std::vector<irep_idt> goto_tracet::get_all_property_ids() const
+std::set<irep_idt> goto_tracet::get_failed_property_ids() const
 {
-  std::vector<irep_idt> property_ids;
+  std::set<irep_idt> property_ids;
   for(const auto &step : steps)
   {
-    if(step.is_assert())
-      property_ids.push_back(step.property_id);
+    if(step.is_assert() && !step.cond_value)
+      property_ids.insert(step.property_id);
   }
   return property_ids;
 }

src/goto-programs/goto_trace.h

@@ -201,8 +201,8 @@ class goto_tracet
     return steps.back();
   }
 
-  /// Returns the property IDs of all assertions in the trace
-  std::vector<irep_idt> get_all_property_ids() const;
+  /// Returns the property IDs of all failed assertions in the trace
+  std::set<irep_idt> get_failed_property_ids() const;
 };
 
 /// Options for printing the trace using show_goto_trace