From 38a13fe227e6b59a49509d4b5ae6618b4c14937a Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 27 Jun 2013 15:35:24 -0400
Subject: Remove output.h from public space, to avoid clashes with symbols
 defined in users' space.

Specifically, output.h was moved to CVC4's "private-library" rules, which means that it's
not installed on users' machines, and public headers should not include it.

Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
---
 test/unit/expr/expr_public.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test/unit/expr/expr_public.h')

diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index c66b5cb1f..7f6385d36 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -342,7 +342,7 @@ public:
   void testIsConst() {
     /* bool isConst() const; */
 
-    Debug.on("isConst");
+    //Debug.on("isConst");
 
     TS_ASSERT(!a_bool->isConst());
     TS_ASSERT(!b_bool->isConst());
-- 
cgit v1.2.3