From 0fcb0b64922be33275aae605c1a6ad9f8c194644 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 22 Oct 2025 12:45:37 +0000 Subject: [PATCH] Fix unit tests for infinite base sorts Updated test to check is_infinite() instead of is_very_big() for FiniteSet(Int) since infinite element sorts now result in infinite FiniteSet sorts (not very_big). Also updated comment to clarify the behavior. Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/finite_set_decl_plugin.cpp | 2 +- src/test/finite_set.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp index d0aa5d976..388e85d4f 100644 --- a/src/ast/finite_set_decl_plugin.cpp +++ b/src/ast/finite_set_decl_plugin.cpp @@ -101,7 +101,7 @@ sort * finite_set_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, par } } else { - // If element sort is infinite or very_big, the finite_set is also very_big + // If element sort is infinite or very_big, the finite_set has the same size sz = elem_sz; } diff --git a/src/test/finite_set.cpp b/src/test/finite_set.cpp index db5490552..0d113b15d 100644 --- a/src/test/finite_set.cpp +++ b/src/test/finite_set.cpp @@ -255,14 +255,14 @@ static void tst_finite_set_sort_size() { sort_size const& bv5_set_sz = finite_set_bv5->get_num_elements(); ENSURE(bv5_set_sz.is_very_big()); - // Test 4: Int sort (infinite) -> FiniteSet(Int) should be very_big + // Test 4: Int sort (infinite) -> FiniteSet(Int) should be infinite arith_util arith(m); sort_ref int_sort(arith.mk_int(), m); parameter int_param(int_sort.get()); sort_ref finite_set_int(m.mk_sort(fsets.get_family_id(), FINITE_SET_SORT, 1, &int_param), m); sort_size const& int_set_sz = finite_set_int->get_num_elements(); - ENSURE(int_set_sz.is_very_big()); + ENSURE(int_set_sz.is_infinite()); // Test 5: BV with size 4 -> BV[4] has 2^4 = 16 elements // FiniteSet(BV[4]) should have 2^16 = 65536 elements