From 491b379adcbd0897c6f9ab5660d4d23afde3abb9 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Sun, 3 Mar 2013 21:08:38 -0800
Subject: [PATCH] refactor DBG_ENABLED() vs. verbose

Always set 'verbose' when we are compiling a DEBUG build.
---
 main.cc  | 2 +-
 model.cc | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/main.cc b/main.cc
index dc3f6f4..b6e4152 100644
--- a/main.cc
+++ b/main.cc
@@ -22,7 +22,7 @@ static void param_defaults(struct model_params *params)
 	params->bound = 0;
 	params->maxfuturevalues = 0;
 	params->expireslop = 10;
-	params->verbose = 0;
+	params->verbose = !!DBG_ENABLED();
 }
 
 static void print_usage(struct model_params *params)
diff --git a/model.cc b/model.cc
index 62550da..0a5cda5 100644
--- a/model.cc
+++ b/model.cc
@@ -530,7 +530,7 @@ void ModelChecker::print_execution(bool printbugs) const
 {
 	print_program_output();
 
-	if (DBG_ENABLED() || params.verbose) {
+	if (params.verbose) {
 		model_print("Earliest divergence point since last feasible execution:\n");
 		if (earliest_diverge)
 			earliest_diverge->print();
@@ -574,7 +574,7 @@ bool ModelChecker::next_execution()
 	record_stats();
 
 	/* Output */
-	if (DBG_ENABLED() || params.verbose || (complete && have_bug_reports()))
+	if (params.verbose || (complete && have_bug_reports()))
 		print_execution(complete);
 	else
 		clear_program_output();
-- 
2.34.1