diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-10-05 19:03:23 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-10-05 19:03:23 +0000 |
| commit | 9bdf1355af20c4dd2b97ea9bc5f34cc20fbdde0f (patch) | |
| tree | 14d79d068e703cf94c632f3fb2e9b5c28cf3872d /src/expr/node.h | |
| parent | ac622612653b3a5edfa981a9e3ef165f34258313 (diff) | |
minor visibility fixes
Diffstat (limited to 'src/expr/node.h')
| -rw-r--r-- | src/expr/node.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index 0f4b55d4a..9d852f195 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -52,6 +52,11 @@ class NodeManager; template <bool ref_count> class NodeTemplate; +// For some reason these are instantiated with different visibility in different modules?? +// Fix by making their instantiations explicit, here. +template <> CVC4ostream& CVC4ostream::operator<<(NodeTemplate<false> const& t) CVC4_PUBLIC; +template <> CVC4ostream& CVC4ostream::operator<<(NodeTemplate<true> const& t) CVC4_PUBLIC; + /** * Exception thrown during the type-checking phase, it can be * thrown by node.getType(). |