use DEBUG define for debugging output

Daniel Kroening · Daniel Kroening · commit a74e05168408 · 2018-09-21T21:30:16.000+01:00
diff --git a/src/goto-symex/show_vcc.cpp b/src/goto-symex/show_vcc.cpp
@@ -62,8 +62,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
`@@ -62,8 +62,8 @@ void show_vcc_plain(`
`62`	`62`	`{`
`63`	`63`	`out << "{-" << count << "} " << format(p_it->cond_expr) << '\n';`
`64`	`64`
`65`		`-#if 0`
`66`		`- out << "GUARD: " << format(p_it->guard_expr) << '\n';`
	`65`	`+#ifdef DEBUG`
	`66`	`+ out << "GUARD: " << format(p_it->guard) << '\n';`
`67`	`67`	`out << '\n';`
`68`	`68`	`#endif`
`69`	`69`