model: print bug reports only for feasible executions

We can assert a bug (e.g., uninitialized load) without having a feasible
exeuction. If this execution is later ruled infeasible, we don't need to
print the trace info.

diff --git a/model.cc b/model.cc
index 0bd8fd3e604528f164846a4bd051815eff9ae3fe..478d1e3b4af2fb26000f9c936400c791c02eada1 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -499,7 +499,7 @@ bool ModelChecker::next_execution()
        record_stats();
 
        /* Output */
-       if (DBG_ENABLED() || params.verbose || have_bug_reports())
+       if (DBG_ENABLED() || params.verbose || (complete && have_bug_reports()))
                print_execution(complete);
        else
                clear_program_output();