diff options
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 006895df7..f0a1e740f 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -21,6 +21,7 @@ #include <typeinfo> #include <vector> +#include "expr/dtype.h" #include "expr/node_manager_attributes.h" #include "options/bv_options.h" #include "options/language.h" @@ -246,7 +247,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::DATATYPE_TYPE: { - const Datatype& dt = (NodeManager::currentNM()->getDatatypeForIndex( + const DType& dt = (NodeManager::currentNM()->getDTypeForIndex( n.getConst<DatatypeIndexConstant>().getIndex())); if (dt.isTuple()) { |