From 98e1f5ca2d601dd3b45ca6d8d7832cf0fcd7a3e4 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Sun, 12 Jul 2026 21:56:12 -0700
Subject: [PATCH] Fix assertion violation in bv2int_translator with
 smt.bv.solver=2 (#10109)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`ASSERTION VIOLATION` at `bv2int_translator.h:72` when using
`smt.bv.solver=2` with formulas containing `abs` (or other arith
expressions that rewrite to ITE with arith predicates).

**Root cause**

`ensure_translated` skips adding sub-expressions of boolean non-BV nodes
to the `todo` list — correct, since the base theory owns them in plugin
mode. However, `translate_expr`'s early-return only covered
`basic_family_id` booleans, not non-basic ones (e.g.,
`arith_family_id`).

When `(abs f)` is rewritten by the arith rewriter to `(ite (>= f 0) f (-
f))`, the predicate `(>= f 0)` ends up in `todo` (as a child of the
ITE), but its own children (e.g., the integer literal `0`) are not
added. `translate_expr` then calls `translated(0)` on an unmapped
expression, firing `SASSERT(r)`.

Reproducer:
```smt2
(declare-const f Int)
(assert (= 0 (mod 0 (bv2nat ((_ int_to_bv 1) (abs f))))))
(check-sat)
; z3 test.smt2 smt.bv.solver=2  →  ASSERTION VIOLATION (before fix)
```

**Fix**

Extend the early-return in `translate_expr` to match
`ensure_translated`'s skip condition — all boolean non-BV expressions in
plugin mode map to themselves:

```cpp
// before
if (m_is_plugin && ap->get_family_id() == basic_family_id && m.is_bool(ap)) {

// after
if (m_is_plugin && m.is_bool(ap) && ap->get_family_id() != bv.get_family_id()) {
```

BV boolean predicates (`bvule`, etc.) are unaffected — they still route
through `translate_bv`.

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
---
 src/ast/rewriter/bv2int_translator.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ast/rewriter/bv2int_translator.cpp b/src/ast/rewriter/bv2int_translator.cpp
index da15bde2bd..042e018558 100644
--- a/src/ast/rewriter/bv2int_translator.cpp
+++ b/src/ast/rewriter/bv2int_translator.cpp
@@ -90,7 +90,7 @@ void bv2int_translator::translate_expr(expr* e) {
         translate_var(to_var(e));
     else {
         app* ap = to_app(e);
-        if (m_is_plugin && ap->get_family_id() == basic_family_id && m.is_bool(ap)) {
+        if (m_is_plugin && m.is_bool(ap) && ap->get_family_id() != bv.get_family_id()) {
             set_translated(e, e);
             return;
         }