summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorDejan Jovanović <dejan.jovanovic@gmail.com>2011-03-30 21:47:12 +0000
committerDejan Jovanović <dejan.jovanovic@gmail.com>2011-03-30 21:47:12 +0000
commitaf976fc656590dbbbfbcdfa45da5dbdab51f4c1c (patch)
treeb0963c89f67a670aa2f32a43dad6da8c2477b02b /src
parenteb058369e08b17c51d0267c87890edd8c41255c2 (diff)
adding CVC4:: qualifier to the #define for debugging so that it can be used outside of CVC4 namespace (like minisat)
Diffstat (limited to 'src')
-rw-r--r--src/util/output.h4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/util/output.h b/src/util/output.h
index b205d1d37..0b1c86afd 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -275,7 +275,7 @@ extern DebugC DebugChannel CVC4_PUBLIC;
#ifdef CVC4_DEBUG
# define Debug DebugChannel
#else /* CVC4_DEBUG */
-# define Debug __cvc4_true() ? debugNullCvc4Stream : DebugChannel
+# define Debug CVC4::__cvc4_true() ? CVC4::debugNullCvc4Stream : CVC4::DebugChannel
#endif /* CVC4_DEBUG */
/** The warning output singleton */
@@ -292,7 +292,7 @@ extern TraceC TraceChannel CVC4_PUBLIC;
#ifdef CVC4_TRACING
# define Trace TraceChannel
#else /* CVC4_TRACING */
-# define Trace __cvc4_true() ? debugNullCvc4Stream : TraceChannel
+# define Trace CVC4::__cvc4_true() ? CVC4::debugNullCvc4Stream : CVC4::TraceChannel
#endif /* CVC4_TRACING */
// Disallow e.g. !Debug("foo").isOn() forms
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback