[Soundness] Daily Soundness Bug Report - January 27, 2026

[github-actions[bot]]

Summary

Workflow Status: Scheduled run completed with limited execution capability
Issues Scanned: 35 soundness-related open issues identified
Test Cases Extracted: 3 new issues documented (total: 4 issues)
Reproduction Status: Unable to execute - missing build tools

Critical Finding: Build Environment Issue

The workflow cannot build Z3 in the GitHub Actions environment. This has been a persistent issue across multiple runs:

MKException: 'ar (archive tool) was not found'
```

**Missing tools**: `ar`, `gcc`, `g++`, `cmake`, `make`

This prevents actual reproduction and validation of soundness bugs. Test case extraction and documentation continue to work.

---

## New Issues Processed (January 27, 2026)

### 🔴 Critical: Issue #8292 - ASSERTION VIOLATION
**Title**: ASSERTION VIOLATION File: ../src/util/mpzzp.h Line: 139  
**Status**: Open, assigned to `@NikolajBjorner` and `@levnach`  
**Severity**: Critical - causes crash in debug build  

**Description**: Assertion violation when running Z3 debug build on complex quantified formula with Real arithmetic and `to_int`/`to_real` conversions.

**Test case**: Extracted to `/tmp/gh-aw/agent/soundness-tests/issue-8292.smt2`

**Error**:
```
ASSERTION VIOLATION
File: ../src/util/mpzzp.h
Line: 139
is_p_normalized(a) && is_p_normalized(b)

Logic: Quantified formulas with Real arithmetic, to_int, to_real, is_int
Commit: 7f91a33

---

🔴 Critical: Issue #8183 - Incorrect UNSAT in Real-to-FP

Title: [Refutational Soundness Bug] Incorrect UNSAT in Real-to-FP conversion with RNE/RNA overflow
Status: Open
Severity: Critical - refutational soundness bug
Labels: Floats

Description: Z3 incorrectly returns unsat for a satisfiable formula involving Real-to-FloatingPoint conversion. The issue is specific to RNE (Round to Nearest Even) and RNA (Round to Nearest Away) rounding modes when handling negative overflow.

Test case: Extracted to /tmp/gh-aw/agent/soundness-tests/issue-8183.smt2

Key observations:

• ✅ Works correctly with RTN (Round Toward Negative) rounding mode
• ❌ Fails with RNE and RNA rounding modes
• ✅ cvc5 correctly returns sat with range hints
• Related to IEEE 754-2008 Section 7.4 Overflow handling

Logic: Real to FloatingPoint conversion
Commit: eca8e19

---

🟡 High: Issue #8194 - Invalid Model with Proof Generation

Title: Incorrect model with :produce-proofs true involving String Theory and UF
Status: Open
Severity: High - incorrect model generation

Description: Z3 reports sat but generates an invalid model when proof generation is enabled. The issue is strictly related to the :produce-proofs true option.

Test case: Extracted to /tmp/gh-aw/agent/soundness-tests/issue-8194.smt2

Key observations:

• ❌ Invalid model with :produce-proofs true
• ✅ Valid model without proof generation
• Model validation error: "an invalid model was generated"

Logic: String theory with uninterpreted functions
Commit: 888d2fc

---

Previously Processed Issues

Issue #8345 (from January 26, 2026)

Title: Soundness issue by converting from bit representation to fp to Real
Status: Extraction successful, reproduction blocked by build failure
Severity: Critical
Labels: Floats

---

Overall Statistics

• Total runs: 2
• Total issues processed: 4
• Successful reproductions: 0 (blocked by build environment)
• Test cases extracted: 4
• Build failures: 2/2 runs

---

Patterns Observed

Floating Point Issues (3/4 issues)

Multiple soundness bugs involve floating-point operations:

• Real-to-FP conversion ([Refutational Soundness Bug] Incorrect UNSAT in Real-to-FP conversion with RNE/RNA overflow #8183, Soundness issue by converting from bit representation to fp to Real #8345)
• FP-to-Real conversion (Soundness issue by converting from bit representation to fp to Real #8345)
• Rounding mode handling (RNE, RNA)
• Overflow/infinity handling

Proof Generation Issues (1/4 issues)

Issue #8194 shows that proof generation can introduce model correctness problems in string theory.

Arithmetic Complexity (1/4 issues)

Issue #8292 involves complex interactions between quantifiers and mixed Real/Int arithmetic with to_int/to_real.

---

Recommendations

1. Fix Build Environment (Highest Priority)

The workflow needs a GitHub Actions runner with C++ build tools installed:

- name: Install build tools
  run: sudo apt-get update && sudo apt-get install -y build-essential cmake

Without this, the workflow can only extract and document test cases, not reproduce or validate them.

2. Prioritize Floating-Point Issues

Three of four identified soundness bugs involve floating-point operations, suggesting this area needs attention.

3. Review Proof Generation Impact

Issue #8194 suggests proof generation may affect model construction in string theory. This interaction should be investigated.

4. Consider Automated Test Suite

Once the build environment is fixed, extracted test cases could be integrated into Z3's regression test suite to prevent regressions.

---

Test Cases Available

All extracted test cases are documented with:

• Full SMT-LIB2 input
• Expected behavior
• Observed behavior
• Relevant commits
• Severity assessment

Location: /tmp/gh-aw/agent/soundness-tests/

Files:

• issue-8292.smt2 - ASSERTION VIOLATION
• issue-8194.smt2 - Invalid model with proofs
• issue-8183.smt2 - Incorrect UNSAT in Real-to-FP
• issue-8345.smt2 - Soundness in FP/Real conversion (from previous run)
• README.md - Documentation

---

Next Steps

1. Address build environment to enable actual reproduction
2. Continue monitoring open soundness issues (35 total found)
3. Extract additional test cases from remaining high-priority issues
4. Re-validate fixed issues once builds succeed

---

Workflow Run: #21396107690
Commit: de44585

AI generated by Soundness Bug Detector

• expires on Feb 3, 2026, 11:58 AM UTC