The example is copied to the build directory during configuration.
You can execute it using
    python example.py
in the build directory after you build Z3.

Proof regression testing
------------------------

The proof matrix runner, its tests, and the proof canaries live in Z3Prover/z3test:
https://github.com/Z3Prover/z3test/blob/master/scripts/proofs/README.md

Z3's CI invokes those tests against the freshly built Z3 executable and runs
the canary lists in the releaseClang configuration. The prooflogs.py and
proofreplay.py examples remain here.

Native Boolean proof certificates
--------------------------------

proof_certificate.py exports a native Z3 proof DAG as JSON. It is a first
milestone toward independent proof checking, not a Lean proof or a verified
unsat verdict. Every bundle explicitly has verification = "unverified".
For propositional input it uses the legacy proof objects in a separate
proof-enabled context and does not change global settings. For linear real
arithmetic and for uninterpreted functions it rebuilds the sat.smt clause log
instead; see "Linear real arithmetic through the clause log" below.

Build the local Python bindings and examples:

    cmake -G Ninja -S . -B build -DCMAKE_BUILD_TYPE=Release \
        -DZ3_BUILD_PYTHON_BINDINGS=ON
    ninja -C build build_z3_python_bindings build_z3_python_examples

From the repository root, export a proof:

    PYTHONPATH=build/python python3 examples/python/proof_certificate.py - \
        > proof.json <<'SMT'
    (set-option :produce-proofs true)
    (declare-const p Bool)
    (assert p)
    (assert (not p))
    (check-sat)
    (get-proof)
    SMT

Pass a filename instead of "-" to read a file. A successful invocation writes
only the JSON bundle to stdout and exits with status 0. Sat, unknown, unsupported
input, missing proofs, and parse errors produce diagnostics on stderr and exit
with status 2, without a bundle. Check the exit status before consuming output.

The Python entry point is export_certificate(source_smt2).

Input scope
-----------

Input is one assertion snapshot, optionally followed by a single check-sat,
get-proof, and exit. Declarations, declare-sort with arity 0, define-fun,
set-logic, set-info, and (set-option :produce-proofs true) are accepted.
Queries with assumptions,
push/pop, multiple queries, commands after a query that change the problem,
and other options or commands are rejected rather than ignored.
Standard semicolon comments, doubled quotes in strings, and quoted symbols are
supported. Quoted symbols have no escape mechanism: backslashes are rejected
and a vertical bar always closes the symbol, matching SMT-LIB 2.5+ and Z3's
scanner. Nonstandard block comments are rejected.

Assertions may use Boolean constants, Boolean variables, not, and, or, implies,
xor, Boolean equality/distinct, and Boolean ite. The qf_lra fragment adds Real
variables and numerals, sums, differences, negation, multiplication by a
constant, division by a nonzero constant, Real-valued ite whose condition is
any supported formula, and the atoms <=, <, >=, >, =, and distinct over Real
terms. The qf_uf fragment adds any number of uninterpreted sorts with
constants, functions, and predicates whose arguments have uninterpreted
sorts or Bool (functions may map between sorts; a Bool argument is any
supported formula), ite terms over a sort whose condition is any supported
formula, and the atoms = and distinct over terms of one sort; it cannot be
combined with arithmetic, functions with Real arguments or results are
rejected, and functions whose arguments are all Bool are accepted only when
the assertions also use an uninterpreted sort (otherwise Z3's sat.smt core
Ackermannizes them with fresh symbols). One symbol name declared with
several signatures is rejected in every fragment: Z3 accepts such overloading
and tells the declarations apart by sort, but the certificate binds symbols
by name, so classification fails for the exporter and again for the
reconstructor, which parses the input itself. Quantifiers, integer arithmetic,
nonlinear terms, bit-vectors, arrays, and pseudo-Boolean operators are
rejected. Definitions are expanded by Z3's parser.
Named assertions are retained as formulas, not converted into extra tracking
assumptions. Declarations unused by the assertions do not affect the fragment.

Bundle format, version 1
-----------------------

    format          "z3-native-proof-dag"
    format_version  1
    z3_version      producer's full Z3 version
    fragment        "propositional", "qf_lra", or "qf_uf"
    result          "unsat" (the producer's result, not a checked claim)
    verification    "unverified"
    source_smt2     original input text
    declarations    native declaration kind, name, domain, range, parameters
    nodes           native applications: declaration index and argument indices
    assertions      node indices of the parsed assertions, in input order
    proof           node index of the native refutation
    rule_counts     counts of distinct proof nodes by native rule name

All indices are zero-based. Nodes are topologically ordered: each argument
refers to an earlier node. Nodes and declarations preserve native identity
and sharing; names are metadata, not identifiers. Proof applications retain
all their arguments, including their conclusions. Declaration kinds are the
Z3_OP_* API constants, not a new set of logical rules.

This version supports application nodes with Bool/Proof sorts and declarations
without parameters. The qf_lra fragment additionally uses the Real sort,
numeral declarations whose name is the exact rational value, the arithmetic
operators and predicates listed above, and th-lemma declarations whose
parameters name a theory hint ("farkas", "bound", "implied-eq", "euf",
"tseitin", "smt", or the exporter's own "cnf") followed, for the first three,
by one nonnegative rational coefficient per literal of the lemma clause.
The qf_uf fragment uses the input's uninterpreted sorts under their own names
(never Bool, Real, or Proof) for constants, function declarations whose
range is one of those sorts and whose domain consists of those sorts and
Bool, predicate declarations over the same domains, and equality and
distinct declarations over one of the sorts; the certificate stays
many-sorted even though Lean sees one type (see below).
Other native shapes are rejected, never serialized incompletely. The root is
required to conclude false, but checking that shape does not establish proof
correctness.

The exporter itself does not verify inference rules. A separate, deliberately
limited Lean reconstruction path is now available below. Theory support and
general proof-required solver integration remain later milestones.

Run the focused regression suite with the local bindings:

    PYTHONPATH=build/python python3 -m unittest discover -s examples/python \
        -p test_proof_certificate.py

Linear real arithmetic through the clause log
--------------------------------------------

The proof objects of the smt core (sat.smt=false) record theory_lra's
arithmetic conflicts as (_ th-lemma arith) without Farkas coefficients, so
they cannot be replayed.
The sat.smt core's clause log carries them: each inferred clause comes with a
hint such as (farkas 1 $11 2 $17 1 $21). proof_certificate.py therefore drives
the z3 executable for arithmetic input and rebuilds the log into the same DAG
format:

    PYTHONPATH=build/python python3 examples/python/proof_certificate.py \
        --z3 build/z3 input.smt2 > proof.json

--core auto (the default) uses the legacy proof object for propositional input
and the clause log otherwise; --core clause-log forces the log for Boolean
input too. --z3 defaults to $Z3_EXE, then build/z3 next to this checkout, then
z3 on PATH; --timeout bounds the solver run in seconds. The executable runs
with sat.smt=true and with solve_eqs, propagate_values, elim_unconstrained, and
bound_simplifier disabled, because the log starts after preprocessing and
bound_simplifier runs solve_eqs internally regardless of its own option.

proof_clause_log.py replays the log with exact bookkeeping and never trusts a
step:

  - Each assumed clause is tied to an original assertion: the identical
    formula is asserted directly; an equivalent formula or conjunct is bridged
    by and-elim, rewrite, and mp; a formula that merely implies the clause,
    which happens when preprocessing splits an xor or an equivalence into
    several clauses, is bridged by a th-lemma with hint "cnf" and one
    unit-resolution. When no single assertion implies the clause (Z3 found a
    contradiction while asserting, or simplified an ite inside one assertion
    under a unit asserted by another, which shows in alldiff clauses), the
    cnf lemma is over an unsat core of the assertions. Clauses with true, not
    false, or complementary literals are def-axiom nodes. Nothing else is
    accepted as an assumption.
  - farkas, bound, implied-eq, and euf hints list literals that are jointly
    contradictory; the exporter emits one th-lemma concluding the clause of
    their complements, after checking farkas and bound coefficients with exact
    rational arithmetic. Equality literals in these hints carry placeholder
    coefficients, so their multipliers are solved for by Gaussian elimination,
    as Z3's own checker does. implied-eq ends in a disequality, not an
    inequality to sum: its shape is checked in Python and Lean proves that
    the preceding literals imply the complementary equality. euf hints may
    also carry congruence claims (cc (= a b)) or (comm (= a b)) that guide
    Z3's checker; they are not literals of the lemma and are dropped after a
    shape check, since Lean's grind performs its own congruence closure.
    tseitin hints list a gate clause and become def-axiom nodes. A bare smt
    hint claims the logged clause outright and becomes a th-lemma with hint
    "smt".
  - A Real ite term is an opaque variable in every Farkas combination, as in
    Z3's arithmetic solver. Its two gate clauses, (not c) or (ite c a b) = a
    and c or (ite c a b) = b, are added as def-axiom nodes and also arrive as
    tseitin inferences; Lean proves them directly from a decidability witness
    for c with ite_eq_left and ite_eq_right.
  - alldiff hints list clauses from internalizing distinct. Like assumed
    clauses, they must be derived from the original assertions; the hint
    itself never authorizes a theorem.
  - rup inferences and every logged clause that differs from its hint's lemma
    are derived by unit propagation over the live clause database, including
    the Tseitin definitions of compound Boolean atoms that Z3's checker also
    uses implicitly. The derivation is emitted as hypothesis, unit-resolution,
    and lemma nodes, so the reconstructor needs no new Boolean rules.
  - del steps remove clauses from the database. If the log never derives the
    empty clause, because the contradiction was found while asserting, the
    empty clause is derived from the assumptions or tied to the assertions.
  - The sat core logs Boolean variables that have no expression, such as
    goal2sat's internal true literal when a unit is asserted, as nullary Bool
    constants k!<n> absent from the input. Assumed and deleted clauses over
    such a phantom are dropped silently: they are tied to no assertion, and
    dropping a clause can only remove support for a later rup step, which
    then fails explicitly. An inference or definition that mentions a phantom
    is rejected as a fresh symbol, as is any other symbol absent from the
    input.

Logs of at least 1 MB are reduced with Z3's native proof trimmer before replay.
The exporter follows the final empty clause's dependency graph, checks it for
missing references and cycles, and replays every retained inference using the
listed premises and independently proved Boolean gate clauses. These
dependencies are untrusted hints, not proof rules. Incorrect trimming must
fail replay or Lean checking. The compact exported DAG keeps every original
assertion, even if its proof is outside the selected refutation.

EUF hints can also contain cc/comm congruence annotations. These are not
additional assumptions: the exported lemma contains only the actual Boolean
literals, and Lean independently proves their inconsistency.

The exporter's own checks only fail early with a clear message; Lean remains
the arbiter.

Uninterpreted functions (QF_UF) go through the same clause log. The log
declares the sort and the functions it uses, which must be the input's own;
function applications are rebuilt with the input's declarations, so a wrong
arity or an ill-sorted argument is rejected. Equality conflicts arrive as
euf hints, distinct as alldiff clauses, and the Boolean structure as tseitin
and rup steps, exactly as for arithmetic; no new hint kind is involved. An
ite term over the sort is an opaque element for the euf core, tied to its
branches by the same two gate clauses as a Real ite, which the replay adds
as def-axiom nodes.

Reconstruct and check a Boolean proof in Lean
-------------------------------------------

proof_to_lean.py consumes the original SMT-LIB file and its native JSON bundle.
It supports asserted, unit-resolution, mp, Boolean rewrite, refl, symm, trans,
trans*, iff-true, iff-false, Boolean monotonicity, and-elim, not-or-elim,
hypothesis, and lemma proof nodes.
It also reconstructs supported Boolean def-axiom clauses.
mp checks its ordered premises and conclusion, accepting implications and
Boolean equivalences. Each rewrite must conclude a Boolean equality/equivalence
and is checked independently of the input hypotheses by a Lean truth table.

refl, symm, and trans check Boolean equivalence endpoints and compose Lean's
logical rules. monotonicity checks identical application heads and arities,
and requires an oriented equivalence for every changed argument. Unchanged
arguments need no premise; repeated arguments can share evidence. Congruence
covers all supported Boolean connectives using direct proof terms, not truth
tables or propositional extensionality. and-elim selects an immediate conjunct.
not-or-elim selects the complement of an immediate disjunct, including native
double-negation cancellation.

iff-true derives (p <-> True) from a proof of p; iff-false derives (p <-> False)
from a proof of (not p). Both validate the premise and ordered endpoints and
use direct Lean logical terms, retaining any open hypothesis dependencies.

trans* finds an equivalence path using only its supplied premises, which may be
reordered, reversed, repeated, cyclic, or redundant. It emits a balanced
composition of Iff.symm and Iff.trans terms without truth tables or solver calls.
Reflexive conclusions permit an empty path. Every premise must be a Boolean
equivalence, even if unused by the chosen path, and disconnected endpoints are
rejected. All supplied premises retain their hypothesis dependencies; choosing
a path does not silently discharge unused assumptions.

hypothesis introduces a temporary assumption, not an original assertion. Open
proof steps are functions of their hypotheses, so a shared subproof can be used
under different lemma scopes without leaking assumptions. lemma requires a proof
of false and a conclusion containing a complement of every open hypothesis.
It supports both complement orientations, compound literals, reordered or
repeated literals, and weakened clauses. All hypotheses of its premise are
discharged; the final proof must have no open hypotheses. Nested lemmas and
shared subproofs use direct Lean proof terms, not truth tables.

def-axiom is not permission to introduce a Lean axiom. Each supported clause is
proved in a separate Lean theorem with no input assertions or proof premises.
Supported shapes are the Boolean gate clauses for not, n-ary and/or, implication,
Boolean equivalence, xor, and Boolean ite, plus complementary literals and
constant tautologies. Negated and compound operands, literal reordering,
duplicates, and weakened clauses are supported. The proof negates the clause
and derives a contradiction from one gate and its immediate operands, without
enumerating assignments to nested atoms. Unsupported or malformed clauses fail
explicitly, even when unused in the final refutation. This is not a general
propositional tautology prover, and fresh-symbol definitions remain unsupported.

th-lemma nodes and arithmetic rewrites are proved by Lean's grind tactic
after unfolding the formula and term definitions they mention; see the
arithmetic section below. Other proof rules, including rewrite*, mp~, and
definition introduction, fail explicitly. Consequently, some otherwise
propositional Z3 refutations are still unsupported.

Install the pinned Lean toolchain as described in lean/README.md. The Boolean
inputs live in Z3Prover/z3test under regressions/proofs/lean/; the commands
below assume a z3test checkout next to this repository. From the repository
root, run this end-to-end example:

    PYTHONPATH=build/python python3 examples/python/proof_certificate.py \
        ../z3test/regressions/proofs/lean/unit_resolution.smt2 > /tmp/unit_resolution.json
    PYTHONPATH=build/python python3 examples/python/proof_to_lean.py \
        ../z3test/regressions/proofs/lean/unit_resolution.smt2 /tmp/unit_resolution.json \
        -o /tmp/unit_resolution.lean

To exercise implication rewriting and mp as well:

    PYTHONPATH=build/python python3 examples/python/proof_certificate.py \
        ../z3test/regressions/proofs/lean/boolean_rewrite.smt2 > /tmp/boolean_rewrite.json
    PYTHONPATH=build/python python3 examples/python/proof_to_lean.py \
        ../z3test/regressions/proofs/lean/boolean_rewrite.smt2 /tmp/boolean_rewrite.json \
        -o /tmp/boolean_rewrite.lean

To also exercise trans, monotonicity, and not-or-elim, replace boolean_rewrite
with boolean_structural in both commands. Use boolean_branching to exercise
hypothesis discharge and learned clauses. Use boolean_def_axiom for clauses
forcing both arguments of an xor to be true, whose native proof still requires
a Boolean gate clause after preprocessing.

The second command invokes scripts/check_lean.sh and publishes the .lean file
only if the pinned Lean checker succeeds. It exits nonzero for malformed or
unsupported certificates, input mismatches, or Lean failures. Existing output
is left unchanged on failure. Output must not alias the original input or JSON
file. Bash and the pinned Lean toolchain must be available.

You can check the resulting Lean file again without Z3:

    ./scripts/check_lean.sh /tmp/unit_resolution.lean

The generated file imports only Init. It contains shared formula definitions
and proof steps built from input hypotheses and Lean core logical rules.
Rewrite lemmas split only the atoms occurring in that rewrite and use
of_decide_eq_true rfl to check every case by kernel reduction, not native_decide
or a solver call. The case count is exponential in a rewrite's atom count;
large rewrites can exceed Lean's normal resource limits and fail without
publishing a proof.

Arithmetic in Lean
------------------

For qf_lra certificates every formula definition takes a second argument
_vars : Nat -> Rat, Real variables become term definitions over it, numerals
become exact Rat literals, and the theorem reads

    theorem unsat (_atoms : Nat -> Prop) (_vars : Nat -> Rat)
        (_h0 : formula_k _atoms _vars) ... : False

Real variables are encoded as Rat. This is sound for the supported fragment:
a system of linear constraints with rational coefficients has a real solution
if and only if it has a rational one, so unsatisfiability over Rat is
unsatisfiability over the reals. The exporter rejects nonlinear terms, which
is the precondition of that argument; extending the fragment must revisit
this encoding. A Real ite becomes Lean's ite over Rat with the classical
decidability instance for its condition, so the term definitions that contain
one are noncomputable; the argument above still applies, because under each
fixed valuation of the conditions the constraints are linear. Every term
definition takes the atom valuation as well as the Rat valuation.

Each th-lemma and each rewrite whose equivalence mentions arithmetic is proved
in a private theorem by unfolding its definitions and calling grind, whose
linear-arithmetic and propositional procedures produce a kernel-checked proof.
Large rewrites first prove a normalized form for each arithmetic atom, then
prove the Boolean equivalence separately over abstract propositions. And/or
rearrangements use projections and case analysis instead of enumerating all
truth assignments or repeatedly invoking arithmetic during Boolean search.
Before Lean runs, the reconstructor re-derives the recorded farkas and bound
combination with exact rationals and rejects coefficients that do not refute
the lemma's literals. grind does not always combine equalities whose constants
are fractions, so the generated proof first states each fractional atom's
denominator-free form as an implication that grind proves, then calls grind
on the lemma; a false helper fails rather than weakening anything. For the
same reason each Real ite reachable from the lemma gets its two branch
equalities, under the condition and under its negation, stated the same way
(scaled to integer coefficients when a branch has fractions) and proved with
ite_eq_left and ite_eq_right; Z3's rewriter can push a comparison through an
ite, in which case these are the only facts tying the ite to its branches.

Lean core's Rat library itself depends on propext, Classical.choice, and
Quot.sound, so arithmetic theorems necessarily report those three standard
axioms. The propositional slice remains axiom-free. Long refutations elaborate
under set_option maxRecDepth 100000; this is an elaborator limit, not a trust
setting.

Refutations with more than 500 proof steps, in every fragment, are split into
separately checked lemmas: one at each shared subproof, and one whenever a
chain would otherwise nest more than 500 steps, because a single nested term
elaborates superlinearly and exhausts Lean's default heartbeat budget between
1,000 and 2,000 steps. Each lemma receives the original assertions as one
conjunction and abstracts its open hypotheses explicitly; steps the root never
uses are not outlined. The final unsat theorem still takes exactly the original
assertions. Arithmetic and uninterpreted-sort lemmas may use classical
decidability, within the already documented standard axiom boundary.
Propositional lemmas instead take the decidability witnesses they need as
parameters, which the final theorem introduces constructively as described
below, so the propositional slice stays axiom-free at every size.

Uninterpreted functions in Lean
-------------------------------

For qf_uf certificates every definition takes, instead of the Rat valuation,
an interpretation of the uninterpreted sorts, all rendered as one type _U:

    theorem unsat (_atoms : Nat -> Prop) (_U : Type) (_elems : Nat -> _U)
        (_funs : Nat -> List _U -> _U) (_preds : Nat -> List _U -> Prop)
        (_bool : Prop -> _U)
        (_h0 : formula_k _atoms _U _elems _funs _preds _bool) ... : False

Constants become _elems i, an application f(a, b) becomes _funs j [a, b], and
a predicate application becomes _preds k [a, b]; equality and distinct are
Lean's = on _U, and an ite over the sort is Lean's ite over _U with the
classical instance, as for Real (its gate clauses are proved the same way).
A Boolean argument p of a function or predicate becomes _bool p, so f(a, p)
is _funs j [a, _bool p]. The theorem quantifies over every type and every indexed
family of functions, so a model of the SMT-LIB input (a nonempty domain with
one function per symbol) is one instance of it: the encoding over-approximates
the class of models and is therefore sound for unsatisfiability. Nothing
relates different indices or different argument lengths, which is exactly the
freedom uninterpreted symbols have. An input with several uninterpreted sorts
is rendered over the same single _U, which is sound for the same reason: a
many-sorted model is an instance of the theorem whose _U is the disjoint
union of the carriers, with each symbol interpreted as in the model on
arguments of its own sorts (and arbitrarily elsewhere). Bool is one more
such sort: its two values join the disjoint union and _bool maps a true
proposition to one and a false one to the other (the instance picks _bool
classically). Every ground term
then denotes its value in the model, and since well-sorted inputs only
compare terms of one sort, every assertion keeps its truth value. Nothing
states that _bool True and _bool False differ, and no Z3 inference needs it:
the euf lemmas over Boolean arguments use only the congruence
p <-> q -> _bool p = _bool q, which grind proves through propext, together
with the two cases of each Boolean argument (Z3's egraph assigns every one
true or false), which each grind lemma states as Classical.em first. This
presumes that each symbol name denotes one many-sorted symbol of the input,
which is why overloading a name across sorts is rejected (see above): the
reconstructor binds symbols by name, requires each bound declaration to
carry the input's full signature (argument and result sorts), interns terms
together with their sort, and checks that the certificate is well-sorted
with respect to the input's own sort names before collapsing them, so an
ill-sorted proof graph is rejected rather than rendered. euf th-lemmas and rewrites over the sorts
are proved by grind, whose congruence closure handles the list applications;
Python only checks shapes for these hints, so a false euf lemma is caught by
Lean alone and the file is not published. grind's proofs here report the same
three standard axioms as the arithmetic slice.

Classical Boolean rewrites, double-negation cancellation in not-or-elim,
def-axiom clauses, and classical steps in lemma discharge use local decidability
witnesses.
The refutation removes these witnesses constructively: given
k : Decidable p -> False, the term
k (isFalse (fun hp => k (isTrue hp))) proves False without assuming decidability.
The final theorem still quantifies over arbitrary Nat -> Prop atom valuations
and takes only the original assertions as hypotheses. Neither it nor the rewrite
and gate-clause lemmas depend on any axioms, sorry, or solver oracles.

The theorem is named unsat inside a namespace derived from the source SHA-256;
the digest is an identifier, not a substitute for checking input equality.
Atoms use generated numeric identifiers, with their original names escaped in
comments. Certificate text is never inserted as executable Lean source.

Trust boundary
--------------

The original file is supplied separately, its text must match source_smt2, and
its parsed assertion DAG must match the certificate's assertion roots exactly,
including order and duplicates. Matching text or result = "unsat" alone does not
authorize a proof. The consumer reparses with Z3's SMT-LIB parser but does not
run Z3's solver search.

Parsing and the Python translation of Boolean expressions, linear
arithmetic, and uninterpreted-function terms into Lean propositions remain
trusted frontend components, not formally verified implementations. Lean
checks the reconstructed theorem, Boolean gate-clause lemmas, rewrite truth
tables, and the grind-proved arithmetic and euf lemmas relative to that
encoding. Boolean equality is encoded as Iff, Boolean xor/ite/distinct as
their logical definitions, Real as Rat under the linearity argument above,
and the uninterpreted sorts as one universally quantified type with indexed
function families. This is not yet a fully formalized SMT-LIB frontend.

The JSON bundle remains marked unverified: successful reconstruction produces
a separate Lean proof artifact rather than changing the producer's claim.

The reconstruction API is reconstruct(source, certificate), which returns
unchecked Lean source, and check_and_write(source, certificate, output), which
checks before publishing. Public API signatures and proof-disabled solving
are unchanged by the preprocessing proof support described below.

Audit preprocessing proof evidence
---------------------------------

proof_preprocessing.py compares two explicit solve-eqs pipelines with proof
generation both disabled and enabled:

    Simplifier("solve-eqs").add(SimpleSolver())
    Then(Tactic("solve-eqs"), Tactic("smt")).solver()

Each run uses a separate context and reports its result, native statistics,
proof terms, rule inventory, and reconstruction/Lean-checking outcome as JSON.
The certificate is always bound to the original input assertions, not the
reduced goal. Checking uses temporary Lean files, which are removed afterward.
This is an opt-in diagnostic, not a replacement exporter or a change to solver
defaults. It currently accepts the same propositional input fragment.

Exercise an essential Boolean equality followed by branching search:

    PYTHONPATH=build/python python3 examples/python/proof_preprocessing.py \
        ../z3test/regressions/proofs/lean/boolean_solve_eqs.smt2 --require-search

Here, removing (= p q) makes the original constraints satisfiable. solve-eqs
eliminates one variable but leaves four clauses; subsequent search reports
positive decision and conflict counts. Also cover goals discharged entirely by
preprocessing, where requiring a search step would be inappropriate:

    PYTHONPATH=build/python python3 examples/python/proof_preprocessing.py \
        ../z3test/regressions/proofs/lean/unit_resolution.smt2

Exit status 0 requires unsat and observed solve-eqs variable elimination in all
four runs, plus successful Lean reconstruction for both proof-enabled runs.
With --require-search, positive decision and conflict counts are also required.
Status 1 reports incomplete coverage or rejected evidence; status 2 indicates an
input, dependency, or invocation error. --timeout-ms bounds each solver check
(default: 10000). Missing statistics mean no execution evidence, not success.

Both examples now exit 0: solve-eqs runs through both interfaces in proof mode,
and the resulting native proofs reconstruct in Lean. Native equality evidence
is carried through extraction, substitution normalization/application, and
solver proof conversion. Congruence proofs are preserved rather than replaced
by unsupported rewrite claims. Boolean unit substitutions use iff-true and
iff-false. Conjunction flattening, replay of eliminated definitions, and tracked
assertions also retain their evidence and original assumption identities.

Proof mode currently supports direct variable equalities, including compound
right-hand sides, and Boolean units. Algebraic/bit-vector isolation, conditional
and nested-equation extraction, and guarded array definitions are skipped until
their own evidence is implemented. A proof-disabled goal still uses the normal
extraction schemes even inside a proof-enabled context. Native support for a
direct equality of another sort does not extend the Lean consumer beyond its
propositional fragment.

Regression coverage includes chained and reversed substitutions, incremental
assertions, push/pop, query assumptions, context translation, and tracked
assertions with single or multiple labels. These are checked against explicit
snapshots of their original active constraints; the exporter still rejects
incremental SMT-LIB scripts and check-sat-assuming.

Preprocessing-only refutations still need checked evidence connecting them to
the original assertions. Conversely, a clausal proof after search only proves
the supplied CNF unless the translation to that CNF is also justified. These
are the two boundaries highlighted in the rutgers-apl/Alivio#1 discussion:
https://github.com/rutgers-apl/Alivio/pull/1#issuecomment-5732956039

Run input-validation/reconstruction tests with the native bindings:

    PYTHONPATH=build/python python3 -m unittest discover -s examples/python \
        -p test_proof_to_lean.py

Include the real Lean integration tests when the pinned toolchain is installed:

    PYTHONPATH=build/python python3 -m unittest discover -s examples/python \
        -p 'test_proof_to_lean*.py'

test_proof_to_lean_arith.py covers the qf_lra slice and test_proof_to_lean_uf.py
the qf_uf slice end to end; both need the z3 executable as well and are
skipped when none is found.

These run in a Lean-enabled Ubuntu CMake CI configuration, not the dependency-free
build-script job.
