Merge pull request diffblue#2623 from diffblue/cbmc-empty-message

Daniel Kroening · web-flow · commit c010edb3340d · 2018-07-27T07:25:26.000+01:00
cbmc: avoid an empty message during result reporting
diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp
@@ -177,9 +177,9 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
             result() << "\n" << "Trace for " << g.first << ":" << "\n";
             show_goto_trace(
               result(), bmc.ns, g.second.goto_trace, bmc.trace_options());
+            result() << eom;
           }
       }
-      result() << eom;
 
       status() << "\n** " << cover_goals.number_covered()
                << " of " << cover_goals.size() << " failed ("

Original file line number	Diff line number	Diff line change
`@@ -177,9 +177,9 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)`
`177`	`177`	`result() << "\n" << "Trace for " << g.first << ":" << "\n";`
`178`	`178`	`show_goto_trace(`
`179`	`179`	`result(), bmc.ns, g.second.goto_trace, bmc.trace_options());`
	`180`	`+ result() << eom;`
`180`	`181`	`}`
`181`	`182`	`}`
`182`		`- result() << eom;`
`183`	`183`
`184`	`184`	`status() << "\n** " << cover_goals.number_covered()`
`185`	`185`	`<< " of " << cover_goals.size() << " failed ("`