summaryrefslogtreecommitdiff
path: root/src/util/dump.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2012-07-12 18:30:15 +0000
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2012-07-12 18:30:15 +0000
commit65798541fa437278cde0c759ab70fd9fa4fe9638 (patch)
tree27341327b8159e58a5ce6371bede6129bf67beb3 /src/util/dump.h
parent78d8b3ce56a1fd243acb54d2aaaf6d716e3b9788 (diff)
merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.
Diffstat (limited to 'src/util/dump.h')
-rw-r--r--src/util/dump.h2
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());
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback