mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-22 15:05:51 +00:00
Code Activity

Fix swapped assert_expr arguments in smt_solver::translate for named assertions (#10135)

Browse source 
With `parallel.enable=true`, Z3 could return a SAT model for a QF_BV
instance that violates its own assertions. The bug traces to solver
translation: named assertions were re-registered with swapped
formula/indicator arguments, corrupting the translated solver's
assertion state.

## Bug

`m_name2assertion` stores `indicator → formula`. In
`smt_solver::translate()`, the structured binding `[k, v]` gives `k =
indicator`, `v = formula`, but `assert_expr(t, a)` expects `(formula,
indicator)`:

```cpp
// Before — args reversed
for (auto& [k, v] : m_name2assertion) {
    expr* val = translator(k);  // indicator
    expr* key = translator(v);  // formula
    result->assert_expr(val, key);  // assert_expr(indicator, formula) ← wrong
}
```

## Fix

```cpp
// After — correct order
for (auto& [k, v] : m_name2assertion) {
    expr* fml = translator(v);  // formula
    expr* ind = translator(k);  // indicator
    result->assert_expr(fml, ind);  // assert_expr(formula, indicator) ✓
}
```

This affects any code path that calls `smt_solver::translate()` and uses
named assertions (`assert_and_track` / `Z3_solver_assert_and_track`),
including all parallel solving modes.

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
Copilot 2026-07-16 13:46:19 -07:00 • committed by GitHub
parent 2a3b64a7f9
commit 63730fefaf
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_solver.cpp
View file

@ -101,9 +101,9 @@ namespace {
result->set_model_converter(mc0()->translate(translator));
for (auto& [k, v] : m_name2assertion) {
expr* val = translator(k);
expr* key = translator(v);
result->assert_expr(val, key);
expr* fml = translator(v);
expr* ind = translator(k);
result->assert_expr(fml, ind);
}
return result;