From 154f71102dfe8715335f51955366cb008c73c25d Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 13 Jul 2026 02:59:45 +0000
Subject: [PATCH] fix: collect type variables (poly_family_id sorts) in
 decl_collector::visit_sort

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.
---
 src/ast/decl_collector.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/ast/decl_collector.cpp b/src/ast/decl_collector.cpp
index a1d472be2c..9beb48ea7e 100644
--- a/src/ast/decl_collector.cpp
+++ b/src/ast/decl_collector.cpp
@@ -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)) {