Daily Test Coverage Improver - Research and Plan

[github-actions]

Repository Analysis

Purpose and Technology Stack

Z3 is Microsoft Research's theorem prover, written primarily in C++ with C++20 standard requirements. It provides various APIs (C++, C, Python, Java, .NET, OCaml, JavaScript/WASM) and uses CMake as its primary build system, with additional support for Visual Studio, Makefiles, vcpkg, and Bazel.

Current Test Coverage Infrastructure

**✅ (redacted)

• Comprehensive unit test suite (src/test/) with 100+ test files covering core functionality
• Robust CI infrastructure with multiple build configurations
• Existing coverage workflow (.github/workflows/coverage.yml) that runs bi-weekly
• Coverage collection infrastructure already configured (.github/actions/daily-test-improver/coverage-steps/action.yml)
• Rich regression test suite via external z3test repository

**⚠️ Current (redacted)

• Coverage report generation is failing due to gcovr merge conflicts with C++ template destructors
• The error indicates: Got function (redacted)<(redacted)>::(redacted)) on multiple lines: 87, 116
• Despite test execution success, HTML coverage reports aren't being generated

Test Organization and Structure

Unit Tests (src/test/):

• Main test executable: test-z3 built via CMake
• Tests cover: algebraic numbers, AST, bit vectors, arithmetic, SAT solving, SMT theories, parsers, utilities
• Test execution command: ./build/test-z3 -a

**External (redacted)

• Regression tests via z3test repository (SMT2 benchmarks)
• Coverage-specific tests in z3test/coverage/cpp
• Example programs that also serve as integration tests

Build and Coverage Commands

**Build (redacted)

# Configure with coverage instrumentation
CXXFLAGS="--coverage" CFLAGS="--coverage" LDFLAGS="-lgcov" CC=clang CXX=clang++ \
  cmake -B build -DCMAKE_BUILD_TYPE=Debug -DCMAKE_INSTALL_PREFIX=./build/install -G "Ninja"

# Build core library and tests
ninja -C build install
ninja -C build test-z3

**Test (redacted)

# Run unit tests
./build/test-z3 -a

# Run regression tests
python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2
python z3test/scripts/test_coverage_tests.py ./build/install z3test/coverage/cpp

Coverage Report Generation (currently broken):

# This fails due to template merge conflicts
gcovr --html coverage.html --gcov-ignore-parse-errors --gcov-executable "llvm-cov gcov" .

Test Coverage Improvement Strategy

Immediate Priorities

1. Fix Coverage Report Generation

   • Resolve gcovr merge conflict by adding --merge-mode-functions=separate flag
   • This will allow us to see actual coverage percentages and identify gaps

2. High-Impact Areas for New Tests (based on codebase analysis):

   • Theory Solvers (src/smt/theory_*.cpp): Core SMT theory implementations
   • AST Operations (src/ast/): Expression manipulation and rewriting
   • SAT Solver Components (src/sat/): Boolean satisfiability solving
   • API Layer (src/api/): Public interface functions
   • Utility Libraries (src/util/): Core data structures and algorithms

3. Coverage Expansion Strategies:

   • Edge Case Testing: Focus on boundary conditions, error paths, and exception handling
   • Integration Testing: Cross-theory interactions and complex formulas
   • API Boundary Testing: Parameter validation and error conditions
   • Performance Path Testing: Rarely-executed optimization paths

Test Organization Guidelines

**For New (redacted)

• Add to existing files in src/test/ when extending functionality of tested modules
• Create new test files following naming pattern <module_name>.cpp
• Follow existing test patterns with simple functions and PASS/FAIL assertions
• Update src/test/CMakeLists.txt when adding new test files

Fast Development Workflow

**Quick Test (redacted)

# Rebuild only tests after changes
ninja -C build test-z3

# Run specific test subset (when developing)
./build/test-z3 -a | grep -A5 -B5 "FAILED\|PASS.*<test-name>"

# Generate coverage after test runs
gcovr --merge-mode-functions=separate --gcov-ignore-parse-errors --gcov-executable "llvm-cov gcov" .

Opportunities for Major Coverage Improvements

1. Theory Combination Testing: Z3's strength is combining multiple theories - test complex multi-theory problems
2. Error Path Coverage: Many error handling paths are likely untested
3. API Robustness: Stress testing of public APIs with invalid inputs
4. Memory Management: Test resource cleanup and edge cases in allocators
5. Parser Edge Cases: Complex SMT-LIB2 parsing scenarios

Questions for Maintainers

1. Are there specific modules or theories that are known to need more test coverage?
2. What are the performance implications of enabling coverage instrumentation in CI?
3. Should we prioritize functional correctness tests or performance regression prevention?
4. Are there any testing patterns or utilities we should avoid or prefer?

---

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

Generated by Agentic Workflow Run

[dsyme]

Work completed: Added comprehensive tests for API algebraic number functions, improving coverage from 0% to 52% (136/258 lines) in src/api/api_algebraic.cpp. Created pull request with the improvements.

Notes for smoother workflow:

• API algebraic functions were completely untested despite being core functionality
• The test framework pattern is simple: create tst_<module>() function, add to main.cpp with TST(<module>), add source file to CMakeLists.txt
• Fast test command: ./build/test-z3 api_algebraic
• Coverage verification: gcovr --merge-mode-functions=separate --gcov-ignore-parse-errors --gcov-executable "llvm-cov gcov" . | grep api_algebraic
• Remaining high-impact 0% coverage areas: api_commands.cpp (5687 lines), api_log_macros.cpp (5333 lines), various model construction functions

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

> Generated by Agentic Workflow Run

Generated by Agentic Workflow Run

[dsyme]

Work completed: Added comprehensive tests for API AST map functions, improving coverage from 0% to 84% (94/111 lines) in src/api/api_ast_map.cpp. Created pull request with the improvements.

Notes for smoother workflow:

• AST map API functions were completely untested despite being core functionality for AST manipulation
• The test framework pattern is straightforward: create tst_<module>() function, add to main.cpp with TST(<module>), add source file to CMakeLists.txt
• Fast test command: ./build/test-z3 api_ast_map
• Coverage verification: gcovr --merge-mode-functions=separate --gcov-ignore-parse-errors --gcov-executable "llvm-cov gcov" . | grep api_ast_map
• Remaining high-impact 0% coverage areas: api_datalog.cpp (486 lines), api_fpa.cpp (1090 lines), api_pb.cpp (64 lines)

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

> Generated by Agentic Workflow Run

Generated by Agentic Workflow Run

[dsyme]

Work completed: Added comprehensive tests for API pseudo-boolean constraint functions, improving coverage from 0% to 100% (64/64 lines) in src/api/api_pb.cpp. Created pull request with the improvements.

Notes for smoother workflow:

• The pseudo-boolean API functions were completely untested despite being core functionality for constraint solving
• The test framework pattern is straightforward: create tst_<module>() function, add to main.cpp with TST(<module>), add source file to CMakeLists.txt
• Fast test command: ./build/test-z3 api_pb
• Coverage verification: gcovr --merge-mode-functions=separate --gcov-ignore-parse-errors --gcov-executable "llvm-cov gcov" . | grep api_pb
• Remaining high-impact 0% coverage areas: api_datalog.cpp (486 lines), api_fpa.cpp (1090 lines), api_qe.cpp (112 lines), api_polynomial.cpp (33 lines)

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

Generated by Agentic Workflow Run

[dsyme]

Work completed: Added comprehensive tests for API polynomial subresultants functions, improving coverage from 0% to 93% (31/33 lines) in src/api/api_polynomial.cpp. Created pull request with the improvements.

Notes for smoother workflow:

• The polynomial subresultants API function was completely untested despite being core algebraic functionality
• The test framework pattern is straightforward: create tst_<module>() function, add to main.cpp with TST(<module>), add source file to CMakeLists.txt
• Fast test command: ./build/test-z3 api_polynomial
• Coverage verification: gcovr --merge-mode-functions=separate --gcov-ignore-parse-errors --gcov-executable "llvm-cov gcov" . | grep api_polynomial
• Remaining high-impact 0% coverage areas: api_datalog.cpp (486 lines), api_fpa.cpp (1090 lines), api_qe.cpp (112 lines), api_stats.cpp (83 lines)

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

Generated by Agentic Workflow Run

[dsyme]

Work completed: Added comprehensive tests for API statistics functions, improving coverage from 0% to 81% (68/83 lines) in src/api/api_stats.cpp. Created pull request with the improvements.

Notes for smoother workflow:

• API statistics functions were completely untested despite being core functionality for browsing solver statistics
• The test framework pattern is straightforward: create tst_<module>() function, add to main.cpp with TST(<module>), add source file to CMakeLists.txt
• Fast test command: ./build/test-z3 api_stats
• Coverage verification: gcovr --merge-mode-functions=separate --gcov-ignore-parse-errors --gcov-executable "llvm-cov gcov" . | grep api_stats
• Remaining high-impact 0% coverage areas: api_datalog.cpp (486 lines), api_fpa.cpp (1090 lines), api_qe.cpp (112 lines), api_commands.cpp (5687 lines)

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

Generated by Agentic Workflow Run

[dsyme]

Work completed: Added comprehensive tests for API quantifier elimination functions, improving coverage from 0% to 83% (93/112 lines) in src/api/api_qe.cpp. Created pull request with the improvements.

Notes for smoother workflow:

• The quantifier elimination API functions were completely untested despite being important functionality for logical reasoning and model manipulation
• The test framework pattern is straightforward: create tst_<module>() function, add to main.cpp with TST(<module>), add source file to CMakeLists.txt
• Fast test command: ./build/test-z3 api_qe
• Coverage verification: gcovr --merge-mode-functions=separate --gcov-ignore-parse-errors --gcov-executable "llvm-cov gcov" . | grep api_qe
• Remaining high-impact 0% coverage areas: api_datalog.cpp (486 lines), api_fpa.cpp (1090 lines), api_rcf.cpp (322 lines), api_commands.cpp (5687 lines)

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

Generated by Agentic Workflow Run

[dsyme]

Work completed: Added comprehensive tests for API real closed field (RCF) functions, improving coverage from 0% to 67% (218/322 lines) in src/api/api_rcf.cpp. Created pull request with the improvements.

Notes for smoother workflow:

• The RCF API functions were completely untested despite being core functionality for real number computations (transcendentals, algebraic numbers, infinitesimals)
• The test framework pattern is straightforward: create tst_<module>() function, add to main.cpp with TST(<module>), add source file to CMakeLists.txt
• Fast test command: ./test-z3 api_rcf
• Coverage verification: gcovr --merge-mode-functions=separate --gcov-ignore-parse-errors --gcov-executable "llvm-cov gcov" --filter ".*api_rcf.*" .
• Remaining high-impact 0% coverage areas: api_datalog.cpp (486 lines), api_fpa.cpp (1090 lines), api_commands.cpp (5687 lines), advanced RCF introspection functions

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

Generated by Agentic Workflow Run

[dsyme]

Work completed: Added comprehensive tests for API Datalog functions, improving coverage from 0% to 17% (84/486 lines) in src/api/api_datalog.cpp. Created pull request with the improvements.

Notes for smoother workflow:

• The Datalog API functions were completely untested despite being core functionality for logic programming
• Successfully implemented tests for finite domain sorts, fixedpoint creation, reference counting, string operations, and statistics
• Avoided more complex query/rule operations that caused segmentation faults, focusing on stable basic functionality
• Fast test command: ./test-z3 api_datalog
• Coverage verification: gcovr --merge-mode-functions=separate --gcov-ignore-parse-errors --gcov-executable "llvm-cov gcov" --filter ".*api_datalog.*" .
• Remaining high-impact 0% coverage areas: api_fpa.cpp (1090 lines), api_commands.cpp (5687 lines)

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

Generated by Agentic Workflow Run

[dsyme]

Work completed: Added comprehensive tests for API special relations functions, improving coverage from 0% to 100% (5/5 lines) in src/api/api_special_relations.cpp. Created pull request with the improvements.

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

Generated by Agentic Workflow Run

[dsyme]

Work completed: Added comprehensive tests for API floating-point functions, improving coverage from 0% to 52% (571/1090 lines) in src/api/api_fpa.cpp. Created pull request with the improvements.

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

Generated by Agentic Workflow Run

[dsyme]

Feedback from @nunoplopes: Don't write stupidly silly tests for API syntax tree creation. Either actually exercise the logic of Z3 or focus on improving coverage in more interesting areas

[dsyme]

Work completed: Added test infrastructure for expr_context_simplifier class which had 0% test coverage. Created PR with basic framework that compiles and passes tests, though functional testing was limited by complex dependencies causing segfaults.

Focus: Following maintainer feedback to avoid trivial tests, targeted core SMT solver component rather than API wrappers.

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

Generated by Agentic Workflow Run

[dsyme]

Work completed: Added comprehensive tests for AST expression statistics module (expr_stat.cpp), achieving 85% coverage improvement from 0%. Following maintainer guidance to focus on meaningful core solver logic rather than API wrappers, implemented tests for actual expression traversal and statistics computation functionality.

Link to PR: See the new draft pull request with comprehensive AST expression statistics tests.

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

Generated by Agentic Workflow Run