Solver timeout silently downgraded to a definitive unsat/error result (error_converter erases ClaripySolverInterruptError)

Description

angr downgrades a solver timeout (z3 returns unknown / resource-out) into a definitive verdict with no signal to the caller, because angr/state_plugins/solver.py's error_converter erases the specific interrupt signal before angr's own handlers can see it.

claripy raises a purpose-built ClaripySolverInterruptError on a solver timeout: a subclass of ClaripyError, not of UnsatError. error_converter wraps every state.solver.* method and catches it under its generic clause:

# angr/state_plugins/solver.py
try:
    return f(*args, **kwargs)
except claripy.UnsatError as e:
    raise SimUnsatError("Got an unsat result") from e
except claripy.ClaripyError as e:                 # <- ClaripySolverInterruptError lands here
    raise SimSolverModeError("Claripy threw an error") from e

So on any solver call made through the standard API, a timeout becomes a generic SimSolverModeError. This defeats the three places angr built to handle a solver interrupt as its own case:

• SimulationManager.step_state → except claripy.ClaripySolverInterruptError → routes the state to the "interrupted" stash + resource_event.
• Explorer._filter_inner → same catch → returns "interrupted".
• The default-enabled Suggestions technique, which watches "interrupted" and logs "your solver timeout fired, consider increasing it" (it reads state.solver._solver.timeout).

None of them can fire: by the time the exception leaves state_plugins/solver.py its type is SimSolverModeError.

Two observable consequences:

(A) Default config. A solver timeout during the per-successor feasibility check (engines/successors.py, not state.satisfiable()) propagates as a generic SimSolverModeError("Claripy threw an error") and the state lands in simgr.errored. angr erases the timeout cause and the Suggestions diagnostic never fires, so the user sees a generic solver error instead of "increase your timeout."

(B) With LAZY_SOLVES. That option defers the feasibility check, so the timeout instead bites during symbolic-jump-target enumeration, where engines/successors.py's except SimSolverModeError: self.unsat_successors.append(state) catches it. angr files the state into simgr.unsat ("proven infeasible"), so it reports a reachable target as a definitive, silent unreachable. LAZY_SOLVES is not a default option, but the in-tree Tracer technique enables it (exploration_techniques/tracer.py, near the end of a trace), so this is a real in-tree caller's path.

angr's own code shows the correct handling by bypassing the wrapper: state_plugins/preconstrainer.py calls .satisfiable() on the raw claripy solver and catches ClaripySolverInterruptError. Same exception, same z3 code: catchable when you bypass the wrapper, erased when you go through the standard state.solver.* API.

Steps to reproduce the bug

jmp rax with rax constrained by a SAT-but-slow cubic (solution rax=0x401000, ~75 ms to solve). A 1 ms solver timeout forces unknown; a generous timeout solves it. Identical inputs; only the timeout differs. The 1 ms value is a deterministic trigger for the same unknown a long solve on a large binary produces.

import logging
import angr
from angr import sim_options as o
logging.getLogger("angr").setLevel(logging.CRITICAL)

proj = angr.load_shellcode(b"\xff\xe0", arch="amd64")  # jmp rax
TARGET = 0x401000
CUBE = (TARGET ** 3) % (2 ** 64)

def step(lazy, timeout_ms):
    opts = {o.LAZY_SOLVES} if lazy else set()
    st = proj.factory.blank_state(addr=0, add_options=opts)
    st.solver.add((st.regs.rax ** 3) % (2 ** 64) == CUBE)  # SAT: rax == 0x401000
    st.solver.add(st.regs.rax > 0x400000)
    st.solver.add(st.regs.rax < 0x402000)
    st.solver._solver.timeout = timeout_ms  # ms
    simgr = proj.factory.simulation_manager(st)
    simgr.step()
    return simgr

# (A) default: 1 ms timeout -> generic error, cause erased, Suggestions cannot fire
s = step(lazy=False, timeout_ms=1)
print("default  1ms :", s, "| errored:", [type(e.error).__name__ for e in s.errored])
print("default 300s :", step(lazy=False, timeout_ms=300000))   # -> 1 active (reachable)

# (B) LAZY_SOLVES: 1 ms timeout -> definitive, SILENT false 'unsat'
print("lazy     1ms :", step(lazy=True, timeout_ms=1))          # -> 1 unsat  (WRONG: reachable)
print("lazy    300s :", step(lazy=True, timeout_ms=300000))     # -> 1 active (reachable)

Observed:

default  1ms : <SimulationManager with 1 errored> | errored: ['SimSolverModeError']
default 300s : <SimulationManager with 1 active>
lazy     1ms : <SimulationManager with 1 unsat>
lazy    300s : <SimulationManager with 1 active>

In every run simgr.interrupted stays empty: direct proof the "interrupted" / Suggestions path never fires.

Environment

Confirmed on the angr suite 9.3.4 (the released wheel, used as a faithful harness):

angr / claripy / cle / pyvex / archinfo : 9.3.4
z3-solver                                : 4.13.0.0
pypcode                                  : 4.0.0
Python                                   : 3.12.13
Platform                                 : linux-x86_64

Re-verified on current master (18aeb23) on 2026-09-17. The load-bearing code is unchanged from the 9.3.4 baseline through master: the re-type clause at state_plugins/solver.py:102-103, the false-unsat catch at engines/successors.py:334-335, and the SimSolverModeError / SimUnsatError hierarchy in errors.py. Happy to paste a bug_report dump from a clean master checkout if useful.

Additional context

One possible starting point: have error_converter re-raise the interrupt rather than fold it into the generic clause, so the "interrupted" / Suggestions path can see it.

try:
    return f(*args, **kwargs)
except claripy.ClaripySolverInterruptError:
    raise                                   # unknown != unsat, != generic error
except claripy.UnsatError as e:
    raise SimUnsatError("Got an unsat result") from e
except claripy.ClaripyError as e:
    raise SimSolverModeError("Claripy threw an error") from e

This is only the shape that worked in my testing, not a claim about the right layer. A few sites catch SimSolverModeError as a generic solver-failure handler, so the interrupt would start propagating past them, and you'd know better than me whether the fix belongs here or somewhere narrower. Happy to open a PR with a regression test in whatever direction you prefer.