Daily Test Coverage Improver: Research and Plan

[github-actions]

Daily Test Coverage Improver: Research and Plan

Repository Summary

Z3 is a theorem prover from Microsoft Research, written in C++ and using C++20 features. The repository provides:

• Core theorem proving functionality
• Multiple language bindings (C++, C, Python, Java, .NET, OCaml, Julia, WebAssembly/TypeScript/JavaScript, Smalltalk)
• Multiple build systems (CMake, Make, Visual Studio, Bazel, vcpkg)
• SMT solver capabilities with SMTLIB2 as the default input format

Current Testing Infrastructure

Test Organization

• Primary test location: src/test/ directory with extensive unit tests
• Test runner: CMake-based test system with test-z3 executable
• Test categories:
  • Unit tests for core components (algebraic, API, arithmetic, AST, etc.)
  • Fuzzing tests in src/test/fuzzing/
  • Linear programming tests in src/test/lp/
  • Integration tests via external z3test repository

Coverage Infrastructure

• Existing coverage setup: .github/workflows/coverage.yml.disabled (currently disabled)
• Coverage tools: gcovr with llvm-cov for detailed HTML reports
• Build configuration: Uses CMake with coverage flags (--coverage, -lgcov)
• Coverage tests: Dedicated coverage test suite via z3test/scripts/test_coverage_tests.py

Build Commands

• CMake build:

  cmake -B build -DCMAKE_BUILD_TYPE=Debug
  cmake --build build --target install
  cmake --build build --target test-z3

• Coverage build:

  CFLAGS="--coverage" CXXFLAGS="--coverage" LDFLAGS="-lgcov" cmake -B build -DCMAKE_BUILD_TYPE=Debug

Test Coverage Improvement Strategy

High-Priority Areas for Coverage Improvement

1. Core solver algorithms - Complex logic in theorem proving components
2. API bindings - Ensure all language bindings are thoroughly tested
3. Edge cases in arithmetic operations - Critical for theorem prover correctness
4. Error handling paths - Improve robustness testing
5. Configuration and parameter handling - Test various solver configurations

Testing Approach

1. Unit test expansion - Add missing unit tests for uncovered functions
2. Property-based testing - Generate test cases for mathematical properties
3. Integration testing - Test end-to-end solver workflows
4. Regression testing - Ensure fixes don't break existing functionality

Coverage Report Generation

# Build with coverage
cmake -B build -DCMAKE_BUILD_TYPE=Debug -DCMAKE_CXX_FLAGS="--coverage" -DCMAKE_C_FLAGS="--coverage" -DCMAKE_EXE_LINKER_FLAGS="-lgcov"
cmake --build build --target install
cmake --build build --target test-z3

# Run tests
cd build && ./test-z3 -a && cd ..

# Generate coverage report
gcovr --html coverage.html --gcov-ignore-parse-errors --gcov-executable "llvm-cov gcov" .
gcovr --html-details coverage-details/ --gcov-ignore-parse-errors --gcov-executable "llvm-cov gcov" -r src --object-directory build

New Ways to Greatly Increase Test Coverage

1. Automated fuzz testing integration - Expand the existing fuzzing infrastructure
2. SMT-LIB benchmark testing - Use standard benchmarks to test more code paths
3. Cross-language binding tests - Ensure parity across different API bindings
4. Performance regression tests - Test that optimizations don't break functionality
5. Parameterized testing - Test various solver configurations and heuristics

Questions for Maintainers

1. Coverage targets: What are acceptable coverage percentage goals for this project?
2. Performance vs coverage: Are there performance-critical paths where extensive testing might be counterproductive?
3. External dependencies: Should tests for external integrations (z3test) be included in coverage?
4. Regression policy: What is the policy for fixing issues discovered during coverage improvement?
5. CI integration: Would you like coverage reporting to be re-enabled in CI?

Implementation Plan

Phase 1: Infrastructure Setup

• Configure coverage collection system
• Establish baseline coverage metrics
• Set up automated coverage reporting

Phase 2: Core Component Testing

• Focus on critical theorem proving algorithms
• Add tests for arithmetic and logical operations
• Improve error handling coverage

Phase 3: API and Integration Testing

• Expand language binding test coverage
• Add end-to-end integration tests
• Test configuration and parameter handling

Phase 4: Edge Cases and Robustness

• Add boundary condition tests
• Improve exception handling coverage
• Test resource exhaustion scenarios

This plan will systematically improve test coverage while maintaining the high quality and performance standards expected of a theorem prover.

> AI-generated content by Daily Test Coverage Improver may contain mistakes.

Generated by Agentic Workflow Run

[NikolajBjorner]

Coverage targets: What are acceptable coverage percentage goals for this project?

Focus first on covering code in the math/lp and math/polynomial directories

Performance vs coverage: Are there performance-critical paths where extensive testing might be counterproductive?

Let us see

External dependencies: Should tests for external integrations (z3test) be included in coverage?

No

Regression policy: What is the policy for fixing issues discovered during coverage improvement?

User visible bugs will be fixed.

CI integration: Would you like coverage reporting to be re-enabled in CI?

Yes. I have added it back. It probably breaks due to bit-rot and that has to be addressed.