diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-09-18 09:53:23 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-18 11:53:23 -0500 |
| commit | 39e395e08646efb2fc0e352bfc110563afbd9043 (patch) | |
| tree | 174c3fbcac3b81b27d1efb49b411490a3142d4ea | |
| parent | e040d5e9e9d8c01138b4b961a1118b7342735d87 (diff) | |
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.
| -rw-r--r-- | src/smt/dump.cpp | 12 | ||||
| -rw-r--r-- | 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 */ |