mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

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.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-02-15 16:27:55 -08:00
parent 784307fc30
commit 943e142bfa
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast_smt_pp.cpp
View file

@ -869,7 +869,7 @@ public:
for (unsigned j = 0; j < f->get_arity(); ++j) { for (unsigned j = 0; j < f->get_arity(); ++j) {
sort* s2 = f->get_domain(j); sort* s2 = f->get_domain(j);
if (!mark.is_marked(s2)) { if (!mark.is_marked(s2)) {
if (s2->get_family_id() == null_family_id) { if (m_manager.is_uninterp(s2)) {
pp_sort_decl(mark, s2); pp_sort_decl(mark, s2);
} }
else if (!util.is_datatype(s2)) { else if (!util.is_datatype(s2)) {