There was an error while loading. Please reload this page.
Document SMT solving and symbolic execution as Boolean function sub-pages Add two core-API pages under Boolean Function: SMT Solving covers the hal_py.SMT interface — constraints, query configuration, results and models — and Symbolic Execution covers the rewriting engine behind simplify_local(), simplify() and evaluate(). Both were verified against a build rather than against the headers, which turned up behavior worth documenting: the timeout is in seconds, solver binaries are looked up at three fixed paths rather than on PATH, symbolic state bindings are write-once, and SymbolicExecution.evaluate() currently raises from Python. Correct the timeout units and the solver lookup on the Simple ALU page accordingly. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>