mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-12 03:44:07 +00:00
Code Activity

Update test to document expected behavior

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-01-27 18:18:13 +00:00
parent db665aa00c
commit 8dbb690eb8
1 changed files with 7 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/test/parametric_datatype.cpp
View file

@ -159,25 +159,22 @@ static void test_parameter_mismatch_error() {
std::cout << "Attempting to instantiate non-parametric datatype with parameters...\n";
// This should either:
// 1. Return nullptr and set an error code, OR
// 2. Throw an exception
// It should NOT segfault
// This should set an error code and return nullptr (or throw exception)
Z3_sort my_list_int = Z3_mk_datatype_sort(ctx, list_name, 1, params);
Z3_error_code err = Z3_get_error_code(ctx);
if (err != Z3_OK) {
std::cout << "Got expected error: " << Z3_get_error_msg(ctx, err) << "\n";
std::cout << "test_parameter_mismatch_error passed (error detected)!\n";
std::cout << "test_parameter_mismatch_error passed!\n";
} else if (my_list_int == nullptr) {
std::cout << "Got nullptr as expected\n";
std::cout << "test_parameter_mismatch_error passed (nullptr returned)!\n";
std::cout << "test_parameter_mismatch_error passed!\n";
} else {
// If we get here, the API didn't properly validate but also didn't crash
std::cout << "Warning: API accepted mismatched parameters without error\n";
// If we get here, something unexpected happened
std::cout << "Warning: Expected error but got valid sort\n";
std::cout << "Result sort: " << Z3_sort_to_string(ctx, my_list_int) << "\n";
// Try to use the sort - this is where the segfault would occur
// We'll skip this for now since we want the test to pass once fixed
// The test still passes because we didn't segfault
std::cout << "test_parameter_mismatch_error passed (no segfault)!\n";
}
Z3_del_context(ctx);