summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r--src/smt/smt_engine.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index fecfba14a..525f90ffe 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -249,7 +249,7 @@ class CVC4_PUBLIC SmtEngine {
* like turning datatypes back into tuples, length-1-bitvectors back
* into booleans, etc.
*/
- Node postprocess(TNode n);
+ Node postprocess(TNode n, TypeNode expectedType);
/**
* This is something of an "init" procedure, but is idempotent; call
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback