From 63730fefaf3ebf78e10d87a245ada591e6c01f1a Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Thu, 16 Jul 2026 13:46:19 -0700
Subject: [PATCH] Fix swapped assert_expr arguments in smt_solver::translate
 for named assertions (#10135)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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>
---
 src/smt/smt_solver.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 393fff202..8bb0e00c3 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -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;