CI Failure DoctorCI Failure: ASSERTION VIOLATION in test_parametric_pair - vector index out of bounds

[github-actions]

🏥 CI Failure Investigation - Run #1179

Summary

The Windows CI workflow (x64 build) failed with an ASSERTION VIOLATION in the new test_parametric_pair test. The failure occurs when accessing datatype constructor accessors for polymorphic/parametric datatypes, resulting in an out-of-bounds vector access at src/util/vector.h:369.

Failure Details

• Run: #1179 (18539389483)
• Commit: 5163411f9b90a339167a41fb3d46a4811420a4db
• Trigger: push (PR Update Z3_mk_datatype_sort API to accept array of sort parameters and add Z3_mk_polymorphic_datatype #7966)
• Workflow: Windows.yml
• Failed Job: build (x64)
• Exit Code: -2147483645

Root Cause Analysis

The failure is triggered by the newly added parametric datatype support in PR #7966. The test test_parametric_pair attempts to:

1. Create a parametric Pair datatype using type variables (alpha, beta)
2. Instantiate the datatype with concrete types via ctx.datatype_sort(pair_name, params)
3. Get constructor accessors using Z3_get_datatype_sort_constructor_accessor

The crash occurs at step 3 when trying to retrieve accessors for the instantiated parametric datatype. The error trace shows:

ASSERTION VIOLATION
test_parametric_pair
Created parametric pair datatype
pair sort: pair
File: D:\a\z3\z3\src\util/vector.h
Line: 369
idx < size()

Technical Analysis

The issue is in src/api/api_datatype.cpp at line 586-602 in Z3_get_datatype_sort_constructor_accessor:

ptr_vector<func_decl> const & decls = *dt_util.get_datatype_constructors(_t);
if (idx_c >= decls.size()) {
    SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
    return nullptr;
}
func_decl* decl = (decls)[idx_c];  // Line 591 - potential crash point
// ...
ptr_vector<func_decl> const & accs = *dt_util.get_constructor_accessors(decl);
SASSERT(accs.size() == decl->get_arity());
if (accs.size() <= idx_a) {
    SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
    RETURN_Z3(nullptr);
}
decl = (accs)[idx_a];  // Line 602 - potential crash point

Problem: When Z3_mk_datatype_sort is called with parameters to instantiate a parametric datatype, it may not properly initialize or return the constructor/accessor information for the instantiated sort. This causes get_datatype_constructors() or get_constructor_accessors() to return empty or incorrectly sized vectors, leading to the out-of-bounds access.

Failed Jobs and Errors

Job: build (x64) - FAILED

• Duration: ~1 hour 2 minutes
• Failed Step: Run Tests (step 6)
• Error: ASSERTION VIOLATION in test_parametric_pair
• Location: src/util/vector.h:369 - idx < size()

Jobs: build (x86), build (amd64_arm64) - SUCCESS

These jobs succeeded because they skip the test execution step.

Investigation Findings

1. New Code: The parametric datatype feature was just added in commit 5163411f
2. Test Location: The failing test appears to be in examples/c++/example.cpp as polymorphic_datatype_example()
3. Missing Test File: The test name test_parametric_pair doesn't exist in the current codebase at src/test/parametric_datatype.cpp, which only contains test_polymorphic_datatype_api
4. API Incompleteness: The updated API Z3_mk_datatype_sort with parameters doesn't properly handle instantiation of parametric datatypes
5. Accessor Retrieval Issue: Z3_get_datatype_sort_constructor_accessor expects the instantiated datatype to have constructor/accessor information, but this information is missing or incomplete

Recommended Actions

• Immediate: Investigate which test is actually named test_parametric_pair (it may be compiled from the C++ example)
• Critical: Fix Z3_mk_datatype_sort to properly initialize constructor/accessor information for instantiated parametric datatypes
• Critical: Update datatype_util::get_datatype_constructors to handle parametric datatype instantiations correctly
• High Priority: Add bounds checking before vector access in Z3_get_datatype_sort_constructor_accessor
• High Priority: Add unit tests specifically for Z3_mk_datatype_sort with parameters
• Medium Priority: Review all datatype utility functions for parametric datatype support
• Medium Priority: Add better error messages when datatype instantiation fails

Specific File Locations for Fixes

1. src/api/api_datatype.cpp:586-602 - Add defensive bounds checking and better error handling
2. src/ast/datatype_decl_plugin.cpp - Review parametric datatype instantiation logic
3. src/api/api_datatype.cpp:438-453 - Review Z3_mk_datatype_sort implementation for parameter handling
4. examples/c++/example.cpp:1009-1096 - Review polymorphic_datatype_example() for correct API usage

Prevention Strategies

1. Pre-merge Testing: Ensure all platform-specific tests run before merging PRs that modify core APIs
2. Comprehensive Test Coverage: Add tests for edge cases in parametric datatype API:
   • Empty parameter lists
   • Multiple instantiations of the same parametric datatype
   • Nested parametric datatypes
   • Accessor retrieval for all instantiation scenarios
3. API Validation: Add runtime checks in Z3_get_datatype_sort_constructor_accessor to validate datatype state
4. Documentation: Document the expected behavior and limitations of parametric datatype instantiation
5. Code Review: Require thorough review of vector accesses in API boundary code

AI Team Self-Improvement

Additional prompting instructions for AI coding agents (copy to instructions.md):

### Parametric Datatypes and Vector Access Safety

When working with Z3's parametric/polymorphic datatype APIs:

1. **Always validate vector bounds** before accessing elements, especially in API boundary code
2. **Test datatype instantiation** with parameters end-to-end, including:
   - Constructor retrieval via `Z3_get_datatype_sort_constructor`
   - Accessor retrieval via `Z3_get_datatype_sort_constructor_accessor`
   - Multiple instantiations with different parameter types
3. **Check for empty vectors** returned from `get_datatype_constructors()` and `get_constructor_accessors()`
4. **Run Windows x64 tests locally** before submitting PRs that modify datatype APIs, as some platforms skip tests
5. **Add defensive assertions** that provide clear error messages rather than relying on vector bounds checks
6. **Document API contracts** for parametric datatypes, especially regarding when constructor/accessor information is available

Historical Context

This is a new type of failure - the first issue encountered with the parametric datatype support feature. There are no similar historical failures in the investigation database.

Related Changes

• PR Update Z3_mk_datatype_sort API to accept array of sort parameters and add Z3_mk_polymorphic_datatype #7966: "Update Z3_mk_datatype_sort API to accept array of sort parameters and add Z3_mk_polymorphic_datatype"
• Author: Copilot + NikolajBjorner
• Changes:
  • Modified Z3_mk_datatype_sort to accept sort parameters
  • Added new Z3_mk_polymorphic_datatype API
  • Updated language bindings (Python, OCaml, .NET, Java)
  • Added example code and tests

---

AI-generated content by CI Failure Doctor may contain mistakes.

Generated by Agentic Workflow Run