From 39e395e08646efb2fc0e352bfc110563afbd9043 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 18 Sep 2020 09:53:23 -0700 Subject: [PATCH] Fix muzzled builds (#5093) Commit 2c2f05c moved some function definitions from dump.h to dump.cpp, which is good. However, the corresponding definitions for muzzled builds weren't moved, so muzzled builds defined the operator << multiple times. This made our nightly competition build fail. This commit fixes the issue by moving the alternative definitions to the source file as well. --- src/smt/dump.cpp | 12 ++++++++++++ src/smt/dump.h | 4 ++-- 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp index 28cf8a34f..ab2bf3bf2 100644 --- a/src/smt/dump.cpp +++ b/src/smt/dump.cpp @@ -24,6 +24,8 @@ namespace CVC4 { +#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) + CVC4dumpstream& CVC4dumpstream::operator<<(const Command& c) { if (d_os != nullptr) @@ -42,6 +44,16 @@ CVC4dumpstream& CVC4dumpstream::operator<<(const NodeCommand& nc) return *this; } +#else + +CVC4dumpstream& CVC4dumpstream::operator<<(const Command& c) { return *this; } +CVC4dumpstream& CVC4dumpstream::operator<<(const NodeCommand& nc) +{ + return *this; +} + +#endif /* CVC4_DUMPING && !CVC4_MUZZLE */ + DumpC DumpChannel CVC4_PUBLIC; std::ostream& DumpC::setStream(std::ostream* os) { diff --git a/src/smt/dump.h b/src/smt/dump.h index ec13a9ae9..832dfb936 100644 --- a/src/smt/dump.h +++ b/src/smt/dump.h @@ -58,8 +58,8 @@ class CVC4_PUBLIC CVC4dumpstream public: CVC4dumpstream() {} CVC4dumpstream(std::ostream& os) {} - CVC4dumpstream& operator<<(const Command& c) { return *this; } - CVC4dumpstream& operator<<(const NodeCommand& nc) { return *this; } + CVC4dumpstream& operator<<(const Command& c); + CVC4dumpstream& operator<<(const NodeCommand& nc); }; /* class CVC4dumpstream */ #endif /* CVC4_DUMPING && !CVC4_MUZZLE */ -- 2.30.2