From 1ec9437f373a6515200263a9d8a4350c0f4d72e2 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 18 Aug 2026 14:22:02 +0300
Subject: [PATCH] Delay Spec lifter argument conversions until exception
 handlers inside lift_fun

In particular, this should fix an issue encountered by Kalmer's QSolvers where the Deadcode exception escaped to the top level due to conv on bottom happening outside the exception handler.
---
 src/lifters/specLifters.ml         | 4 ++--
 src/lifters/wideningTokenLifter.ml | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/lifters/specLifters.ml b/src/lifters/specLifters.ml
index c72d2904cf..e460985fde 100644
--- a/src/lifters/specLifters.ml
+++ b/src/lifters/specLifters.ml
@@ -601,9 +601,9 @@ struct
   let combine_assign man r fe f args fc es f_ask = lift_fun man D.lift S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) `Bot
 
   let threadenter man ~multiple lval f args = lift_fun man (List.map D.lift) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval) []
-  let threadspawn man ~multiple lval f args fman = lift_fun man D.lift (S.threadspawn ~multiple) ((|>) (conv fman) % (|>) args % (|>) f % (|>) lval) `Bot
+  let threadspawn man ~multiple lval f args fman = lift_fun man D.lift (S.threadspawn ~multiple) (fun p -> p lval f args (conv fman)) `Bot (* fun to delay (conv fman) until exception handler inside lift_fun *)
 
-  let event (man:(D.t,G.t,C.t,V.t) man) (e:Events.t) (oman:(D.t,G.t,C.t,V.t) man):D.t = lift_fun man D.lift S.event ((|>) (conv oman) % (|>) e) `Bot
+  let event (man:(D.t,G.t,C.t,V.t) man) (e:Events.t) (oman:(D.t,G.t,C.t,V.t) man):D.t = lift_fun man D.lift S.event (fun p -> p e (conv oman)) `Bot (* fun to delay (conv oman) until exception handler inside lift_fun *)
 end
 
 
diff --git a/src/lifters/wideningTokenLifter.ml b/src/lifters/wideningTokenLifter.ml
index 0001fb2796..1718084b3e 100644
--- a/src/lifters/wideningTokenLifter.ml
+++ b/src/lifters/wideningTokenLifter.ml
@@ -180,6 +180,6 @@ struct
   let combine_assign man r fe f args fc es f_ask = lift_fun man lift' S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) (* TODO: use tokens from es *)
 
   let threadenter man  ~multiple lval f args = lift_fun man (fun l ts -> List.map (Fun.flip lift' ts) l) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval )
-  let threadspawn man ~multiple lval f args fman = lift_fun man lift' (S.threadspawn ~multiple) ((|>) (conv fman) % (|>) args % (|>) f % (|>) lval)
-  let event man e oman = lift_fun man lift' S.event ((|>) (conv oman) % (|>) e)
+  let threadspawn man ~multiple lval f args fman = lift_fun man lift' (S.threadspawn ~multiple) (fun p -> p lval f args (conv fman)) (* fun to delay (conv fman) until exception handler inside lift_fun *)
+  let event man e oman = lift_fun man lift' S.event (fun p -> p e (conv oman)) (* fun to delay (conv oman) until exception handler inside lift_fun *)
 end