From 943e142bfacdba4fafaaeb21c5a5861f8d8fbfd0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 15 Feb 2013 16:27:55 -0800 Subject: [PATCH] Fix bug in ast_smt_pp.cpp. After user_sort_plugin was introduced, it is not that case that if a sort is uninterpreted, then sort->get_family_id() == null_family_id. Signed-off-by: Leonardo de Moura --- src/ast/ast_smt_pp.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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)) {