From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 18 Sep 2020 16:53:23 +0000 (-0700)
Subject: Fix muzzled builds (#5093)
X-Git-Tag: cvc5-1.0.0~2836
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=39e395e08646efb2fc0e352bfc110563afbd9043;p=cvc5.git

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.
---

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 */