diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 5bdc70dc2..5819e3930 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -869,7 +869,7 @@ public: for (unsigned j = 0; j < f->get_arity(); ++j) { sort* s2 = f->get_domain(j); if (!mark.is_marked(s2)) { - if (s2->get_family_id() == null_family_id) { + if (m_manager.is_uninterp(s2)) { pp_sort_decl(mark, s2); } else if (!util.is_datatype(s2)) {