mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

fix: simplify type variable collection condition in decl_collector::visit_sort

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-07-13 03:00:50 +00:00 • committed by GitHub
parent 154f71102d
commit 638e7b7bce
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/decl_collector.cpp
View file

@ -24,9 +24,7 @@ Revision History:
void decl_collector::visit_sort(sort * n) { void decl_collector::visit_sort(sort * n) {
SASSERT(!m_visited.is_marked(n)); SASSERT(!m_visited.is_marked(n));
family_id fid = n->get_family_id(); family_id fid = n->get_family_id();
if (m.is_uninterp(n)) if (m.is_uninterp(n) || fid == poly_family_id)
m_sorts.push_back(n);
else if (fid == poly_family_id)
m_sorts.push_back(n); m_sorts.push_back(n);
else if (fid == m_dt_fid) { else if (fid == m_dt_fid) {
m_sorts.push_back(n); m_sorts.push_back(n);