diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index c6c9c7c0c..420961b4e 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -537,7 +537,7 @@ class smt_printer {
     }
 
     void print_bound(symbol const& name) {
-        if (!m_is_smt2 && (name.is_numerical() || '?' != name.bare_str()[0])) {
+        if (!is_smt2 && (name.is_numerical() || '?' != name.bare_str()[0])) {
             m_out << "?";
         }
         m_out << name;
@@ -561,7 +561,7 @@ class smt_printer {
             m_out << "(";
             print_bound(m_renaming.get_symbol(q->get_decl_name(i)));
             m_out << " ";
-            visit_sort(s, !m_is-smt2);
+            visit_sort(s, true);
             m_out << ") ";
         }
         if (m_is_smt2) {