mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-14 19:15:41 +00:00
Code Activity

fix: collect type variables (poly_family_id sorts) in decl_collector::visit_sort

Browse source 
Type variables created via mk_type_var (e.g. from declare-type-var in SMT-LIB2
or TPTP polymorphic type vars) have poly_family_id. decl_collector::visit_sort
did not add them to m_sorts, so ast_pp_util::display_decls / solver::display
never emitted (declare-sort TypeVar 0) before uses, producing invalid SMT-LIB2.

Fix: add an else-if branch for poly_family_id alongside the existing is_uninterp
branch so type variables are pushed into m_sorts, topologically ordered by
order_deps (they have no dependencies, so they sort first), and declared before
other sorts and func_decls that reference them.
This commit is contained in:
copilot-swe-agent[bot] 2026-07-13 02:59:45 +00:00 • committed by GitHub
parent 0b8335e776
commit 154f71102d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/decl_collector.cpp
View file

@ -26,6 +26,8 @@ void decl_collector::visit_sort(sort * n) {
family_id fid = n->get_family_id();
if (m.is_uninterp(n))
m_sorts.push_back(n);
else if (fid == poly_family_id)
m_sorts.push_back(n);
else if (fid == m_dt_fid) {
m_sorts.push_back(n);
for (func_decl * cnstr : *m_dt_util.get_datatype_constructors(n)) {