use DEBUG define for debugging output

Daniel Kroening · Daniel Kroening · commit 8d3b637a4fda · 2018-10-11T06:21:29.000-04:00
diff --git a/src/goto-symex/show_vcc.cpp b/src/goto-symex/show_vcc.cpp
@@ -65,8 +65,8 @@ void show_vcc_plain(
         {
           out << "{-" << count << "} " << format(p_it->cond_expr) << '\n';
 
-#if 0
-          out << "GUARD: " << format(p_it->guard_expr) << '\n';
+#ifdef DEBUG
+          out << "GUARD: " << format(p_it->guard) << '\n';
           out << '\n';
 #endif
 

Original file line number	Diff line number	Diff line change
`@@ -65,8 +65,8 @@ void show_vcc_plain(`
`65`	`65`	`{`
`66`	`66`	`out << "{-" << count << "} " << format(p_it->cond_expr) << '\n';`
`67`	`67`
`68`		`-#if 0`
`69`		`- out << "GUARD: " << format(p_it->guard_expr) << '\n';`
	`68`	`+#ifdef DEBUG`
	`69`	`+ out << "GUARD: " << format(p_it->guard) << '\n';`
`70`	`70`	`out << '\n';`
`71`	`71`	`#endif`
`72`	`72`