diff options
Diffstat (limited to 'src/util/dump.h')
| -rw-r--r-- | src/util/dump.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/util/dump.h b/src/util/dump.h index 7318af1a5..382092474 100644 --- a/src/util/dump.h +++ b/src/util/dump.h @@ -103,7 +103,7 @@ public: std::string s = ss.str(); CVC4dumpstream(getStream(), d_commands) << CommentCommand(s + " is " + comment) - << DeclareFunctionCommand(s, e.getType()); + << DeclareFunctionCommand(s, e, e.getType()); } } |