From 6f45039487a95c7fb8023a2aa08b9d9085f6985e Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 13 Dec 2012 00:36:04 -0800 Subject: [PATCH] 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. --- model.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/model.cc b/model.cc index 0bd8fd3..478d1e3 100644 --- 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(); -- 2.34.1