From 9438813fa2269889cddee713208c0f3c918b720b Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Sat, 30 May 2026 15:02:51 +0200
Subject: [PATCH] =?UTF-8?q?release:=20v1.1.2=20=E2=80=94=20fix=20#145=20ga?=
 =?UTF-8?q?le=20i64=20SortDiffers=20crash=20(width-match=20+=20Z3=20timeou?=
 =?UTF-8?q?t)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Patch release closing #145: loom optimize panicked with
SortDiffers { BitVec 64 vs 32 } (+ unwrap-None) on i64-heavy modules
(gale-ffi / compiler_builtins), reverting every function and emitting
21 MB+ of stderr. Shipped via PR #146.

- Width-match i64 binops in both symbolic executors (the dormant
  match_bv_widths helper, now wired in). Sound: repairs model artifacts
  at binops; equivalence checks bail conservatively, never force-match.
- Z3 per-query timeout (LOOM_Z3_TIMEOUT_MS, default 5000ms) -> slow i64
  solve becomes a conservative revert, not a hang.
- z3-origin panic backtraces suppressed (Once-installed filter);
  per-function revert logging behind LOOM_VERBOSE_REVERTS. Kills the
  21 MB flood.

Known limitation (tracked #147): fully-verified i64 inlining is slow in
aggregate on large modules; the i64 inline unit tests stay #[ignore]'d
(they hang in SMT-formula construction, not bounded by the per-query
timeout). v1.1.2 guarantees no crash / no flood / sound output;
fast verified i64 inlining + re-enabling the tests is #147.

Trace: REQ-6, REQ-12
---
 CHANGELOG.md | 23 ++++++++++++++++++++++-
 Cargo.toml   |  2 +-
 2 files changed, 23 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d274d61..49e1f50 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,7 +5,28 @@ All notable changes to LOOM will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
-## [Unreleased]
+## [1.1.2] - 2026-05-30
+
+**Bug-fix release: the gale-ffi i64 `SortDiffers` crash (#145).** Closes
+the panic + 21 MB-stderr flood that made `loom optimize` unusable on
+i64-heavy modules (gale-ffi / compiler_builtins), and width-corrects the
+Z3 translation validator's i64 modeling.
+
+### Known limitation (tracked: #147)
+
+Verifying i64 inlining *for real* requires a Z3 bitvector solve per
+function, which is **slow in aggregate** on large i64-heavy modules — so
+`loom optimize` on such a module is bounded-but-slow (each query capped
+by `LOOM_Z3_TIMEOUT_MS`, default 5000 ms → conservative revert on
+timeout), and the i64 inline *unit tests* are `#[ignore]`'d (they hang
+in SMT-formula construction, which the per-query timeout doesn't bound).
+**What this release guarantees:** no crash, no stderr flood, sound output
+(width-correct verification; conservative revert when a proof is slow or
+unprovable). **What it does not yet guarantee:** fast, fully-verified i64
+inlining on large modules. That — a cheaper i64 inline-equivalence check
+and re-enabling the ignored tests — is tracked in #147. Tune with
+`LOOM_Z3_TIMEOUT_MS` (lower = faster, more reverts) and
+`LOOM_Z3_MAX_INSTRUCTIONS` for large i64 workloads.
 
 ### Fixed
 
diff --git a/Cargo.toml b/Cargo.toml
index a8706be..4c442c5 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -9,7 +9,7 @@ members = [
 ]
 
 [workspace.package]
-version = "1.1.1"
+version = "1.1.2"
 authors = ["PulseEngine <https://github.com/pulseengine>"]
 edition = "2024"
 license = "Apache-2.0"