From: Brian Norris <banorris@uci.edu>
Date: Thu, 13 Dec 2012 08:36:04 +0000 (-0800)
Subject: model: print bug reports only for feasible executions
X-Git-Tag: oopsla2013~419
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=6f45039487a95c7fb8023a2aa08b9d9085f6985e;p=model-checker.git

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 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();