use DEBUG define for debugging output

Daniel Kroening · Daniel Kroening · commit 9f24f8310ae7 · 2018-09-21T19:58:22.000+01:00
diff --git a/src/goto-symex/show_vcc.cpp b/src/goto-symex/show_vcc.cpp
@@ -62,7 +62,7 @@ void show_vcc_plain(
         {
           out << "{-" << count << "} " << format(p_it->cond_expr) << '\n';
 
-#if 0
+#ifdef DEBUG
           out << "GUARD: " << format(p_it->guard_expr) << '\n';
           out << '\n';
 #endif

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