summaryrefslogtreecommitdiff
path: root/src/printer/smt2/smt2_printer.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
-rw-r--r--src/printer/smt2/smt2_printer.cpp5
1 files changed, 3 insertions, 2 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index b71e9d4c4..fa49d8973 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -21,6 +21,7 @@
#include <typeinfo>
#include <vector>
+#include "api/cvc4cpp.h"
#include "expr/node_manager_attributes.h"
#include "options/language.h"
#include "options/smt_options.h"
@@ -1754,8 +1755,8 @@ static void toStream(std::ostream& out, const SimplifyCommand* c)
static void toStream(std::ostream& out, const GetValueCommand* c)
{
out << "(get-value ( ";
- const vector<Expr>& terms = c->getTerms();
- copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " "));
+ const vector<api::Term>& terms = c->getTerms();
+ copy(terms.begin(), terms.end(), ostream_iterator<api::Term>(out, " "));
out << "))";
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback