From 30f26d2b83af3c9e3da5b5e4ecd869cba925206b Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sat, 16 Feb 2019 22:23:22 +0000
Subject: [PATCH 1/2] Get_all_property_ids should only return failed properties

Passed properties on traces are less interesting.
---
 src/cbmc/c_test_input_generator.cpp     | 4 ++--
 src/goto-checker/goto_trace_storage.cpp | 2 +-
 src/goto-programs/goto_trace.cpp        | 8 ++++----
 src/goto-programs/goto_trace.h          | 4 ++--
 4 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/cbmc/c_test_input_generator.cpp b/src/cbmc/c_test_input_generator.cpp
index 7ae336d4c6b..0796fbb7722 100644
--- a/src/cbmc/c_test_input_generator.cpp
+++ b/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));
   }
@@ -112,7 +112,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));
diff --git a/src/goto-checker/goto_trace_storage.cpp b/src/goto-checker/goto_trace_storage.cpp
index d59d29ea8e0..38f01afd12f 100644
--- a/src/goto-checker/goto_trace_storage.cpp
+++ b/src/goto-checker/goto_trace_storage.cpp
@@ -33,7 +33,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)
diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp
index 64bbcb1512a..967b2dbc578 100644
--- a/src/goto-programs/goto_trace.cpp
+++ b/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;
 }
diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h
index 99a43478109..2b6dd26ad28 100644
--- a/src/goto-programs/goto_trace.h
+++ b/src/goto-programs/goto_trace.h
@@ -206,8 +206,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

From 94ca5d9c286a02ce06f477a8a6dc1397d35cac61 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Tue, 19 Feb 2019 20:25:37 +0000
Subject: [PATCH 2/2] Add regression test for multiple coverage goal instances

Covered goals is a set of unique elements
---
 regression/cbmc-cover/branch-loop1/main.c    | 11 +++++++++++
 regression/cbmc-cover/branch-loop1/test.desc | 11 +++++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 regression/cbmc-cover/branch-loop1/main.c
 create mode 100644 regression/cbmc-cover/branch-loop1/test.desc

diff --git a/regression/cbmc-cover/branch-loop1/main.c b/regression/cbmc-cover/branch-loop1/main.c
new file mode 100644
index 00000000000..f1f62f1d8bf
--- /dev/null
+++ b/regression/cbmc-cover/branch-loop1/main.c
@@ -0,0 +1,11 @@
+int main(int argc, char **argv)
+{
+  for(int i = 0; i < 4; i++)
+  {
+    char c;
+    __CPROVER_input("c", c);
+    if(c == 42)
+      return 0;
+  }
+  return 1;
+}
diff --git a/regression/cbmc-cover/branch-loop1/test.desc b/regression/cbmc-cover/branch-loop1/test.desc
new file mode 100644
index 00000000000..5eacaa4e600
--- /dev/null
+++ b/regression/cbmc-cover/branch-loop1/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--xml-ui --cover branch
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+</inputs>\n\s*<goal id="main\.coverage\.1"/>\n\s*<goal id="main\.coverage\.2"/>\n\s*<goal id="main\.coverage\.3"/>\n\s*<goal id="main\.coverage\.5"/>\n\s*</test>
+--
+^warning: ignoring
+--
+Expect each goal only occur once per test.