From ec3aafd51eed18d792232c0453ca04a0e7d49337 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 29 Dec 2025 18:09:13 -0800 Subject: [PATCH] fixup parameter to enable pretty printing of range sort Signed-off-by: Nikolaj Bjorner --- src/ast/finite_set_decl_plugin.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp index bb49ff18e..49ee4e2bf 100644 --- a/src/ast/finite_set_decl_plugin.cpp +++ b/src/ast/finite_set_decl_plugin.cpp @@ -161,7 +161,9 @@ func_decl * finite_set_decl_plugin::mk_finite_set_op(decl_kind k, unsigned arity polymorphism::util poly_util(m); sort_ref rng(m); poly_util.match(*m_sigs[k], arity, domain, range, rng); - func_decl_info info(m_family_id, k); + unsigned np = k == OP_FINITE_SET_UNIQUE_SET ? 1 : 0; + parameter p(rng.get()); + func_decl_info info(m_family_id, k, np, &p); if (k == OP_FINITE_SET_UNION || k == OP_FINITE_SET_INTERSECT) { info.set_commutative(true); info.set_associative(true);