diff options
| author |  zinc <zinc@downsta.ir>
| 2026-10-15 05:25:58 +0330 |
|---|---|---|
| committer | zinc <zinc@downsta.ir>
| 2026-10-15 05:25:58 +0330 |
| commit | a6e52065bb7eaee3bbef5a1c3f879c616e3d24bc (patch) | |
| tree | 8527b7d56c0aa2d067c6fb53ea584b2af6d3bdca /tests/programs/bounds_hi.zc | |
| parent | prover: len/cross-array/fixed-new/affine proofs; keep facts past call loops (diff) | |
prover: do not restore length facts after a call-loop
Restoring undirtied lafacts when the body might free was wrong: push can
grow an array without dirtying its name, so a[99] after push warned against
a stale length 0. Keep the old lafact_keep rule; reorder explain_prover so
the constant/affine cases run before the touch() loops.
Diffstat (limited to 'tests/programs/bounds_hi.zc')
0 files changed, 0 insertions, 0 deletions