From 5f2249fa9bb953227c718aa643494dd93754c116 Mon Sep 17 00:00:00 2001
From: Ronald Judin <ronald.judin@ut.ee>
Date: Fri, 24 May 2024 11:16:36 +0300
Subject: [PATCH 01/12] Implement delayed widening

---
 src/domains/lattice.ml                      | 38 +++++++++++
 src/framework/constraints.ml                | 73 +++++++++++++++++++++
 src/framework/control.ml                    |  1 +
 src/util/options.schema.json                |  6 ++
 tests/regression/72-delayed/01-nontrivial.c | 14 ++++
 5 files changed, 132 insertions(+)
 create mode 100644 tests/regression/72-delayed/01-nontrivial.c

diff --git a/src/domains/lattice.ml b/src/domains/lattice.ml
index f1657b32ca..dfe8b4338d 100644
--- a/src/domains/lattice.ml
+++ b/src/domains/lattice.ml
@@ -616,3 +616,41 @@ struct
   let pretty_diff () ((x:t),(y:t)): Pretty.doc =
     Pretty.dprintf "%a not leq %a" pretty x pretty y
 end
+
+module DelayedConf (C: Printable.ProdConfiguration) (Base: S) =
+struct
+  (** n () is an arbitrary constant *)
+  let n () = GobConfig.get_int "ana.widen.delay"
+  module P = (Printable.Chain (struct let n () = n () let names n = (string_of_int n) end))
+
+  include Printable.ProdConf (C) (Base) (P)
+
+  let bot () = (Base.bot (), 0)
+  let is_bot (b, _) = Base.is_bot b
+  let top () = (Base.top (), n ())
+  let is_top (b, _) = Base.is_top b
+
+  let leq (b1,_) (b2,_) = Base.leq b1 b2
+
+  let pretty_diff () (((b1,i1):t),((b2,i2):t)): Pretty.doc =
+    if Base.leq b1 b2 then
+      let f = fun () i -> Pretty.num i in
+      Pretty.dprintf "%a not leq %a" f i1 f i2
+    else
+      Base.pretty_diff () (b1,b2)
+
+  let join (b1,i1) (b2,i2) = (Base.join b1 b2, max i1 i2)
+  let meet (b1,i1) (b2,i2) = (Base.meet b1 b2, max i1 i2)
+  let narrow (b1,i1) (b2,i2) = (Base.narrow b1 b2, max i1 i2)
+  let widen (b1,i1) (b2,i2) =
+    if max i1 i2 < n () then
+      (Base.join b1 b2, 1 + max i1 i2)
+    else
+      (Base.widen b1 b2, max i1 i2)
+
+  let printXml f (b, i) =
+    BatPrintf.fprintf f "%a<analysis name=\"widen-delay\">%a</analysis>" Base.printXml b P.printXml i
+end
+
+module Delayed = DelayedConf (struct let expand_fst = true let expand_snd = true end)
+module DelayedSimple = DelayedConf (struct let expand_fst = false let expand_snd = false end)
\ No newline at end of file
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index d00a530e07..4b2f53cb33 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -1914,3 +1914,76 @@ struct
         Some f'
   end
 end
+
+module Delayed (S:Spec)
+  : Spec with module D = Lattice.Delayed (S.D)
+          and module G = S.G
+          and module C = S.C
+=
+struct
+  module D = Lattice.Delayed (S.D)
+  module G = S.G
+  module C = S.C
+  module V = S.V
+
+  let name () = S.name ()^" delayed"
+
+  let start_level = ref (`Top)
+
+  type marshal = S.marshal (* TODO: should hashcons table be in here to avoid relift altogether? *)
+  let init marshal =
+    S.init marshal
+
+  let finalize = S.finalize
+
+  let should_join (x,_) (y,_) = S.should_join x y
+
+  let startstate v = (S.startstate v, 0)
+  let exitstate  v = (S.exitstate  v, D.n ())
+  let morphstate v (d,l) = (S.morphstate v d, l)
+
+  let context fd (d,_) = S.context fd d
+
+  let conv (ctx: (D.t, G.t, C.t, V.t) ctx) : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
+    { ctx with local = fst ctx.local
+             ; split = (fun d es -> ctx.split (d, snd ctx.local) es )
+    }
+  let lift_fun ctx f g h =
+    f @@ h (g (conv ctx))
+
+  let enter ctx r f args =
+    let liftmap = List.map (fun (x,y) -> (x, snd ctx.local), (y, snd ctx.local)) in
+    lift_fun ctx liftmap S.enter ((|>) args % (|>) f % (|>) r)
+
+  let lift ctx d = (d, 0)
+
+  (* Used only in the threadspawn function. *)
+  let rec lift' ctx dl =
+    match dl with
+    | [] -> []
+    | d::l -> (d, 0)::(lift' ctx l)
+
+  let sync ctx reason = lift_fun ctx (lift ctx) S.sync   ((|>) reason)
+  let query ctx (type a) (q: a Queries.t): a Queries.result = S.query (conv ctx) q
+  let assign ctx lv e = lift_fun ctx (lift ctx) S.assign ((|>) e % (|>) lv)
+  let vdecl ctx v     = lift_fun ctx (lift ctx) S.vdecl  ((|>) v)
+  let branch ctx e tv = lift_fun ctx (lift ctx) S.branch ((|>) tv % (|>) e)
+  let body ctx f      = lift_fun ctx (lift ctx) S.body   ((|>) f)
+  let return ctx r f  = lift_fun ctx (lift ctx) S.return ((|>) f % (|>) r)
+  let asm ctx         = lift_fun ctx (lift ctx) S.asm    identity
+  let skip ctx        = lift_fun ctx (lift ctx) S.skip identity
+  let special ctx r f args        = lift_fun ctx (lift ctx) S.special ((|>) args % (|>) f % (|>) r)
+  let combine_env ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_env (fun p -> p r fe f args fc (fst es) f_ask)
+  let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_assign (fun p -> p r fe f args fc (fst es) f_ask)
+
+  let threadenter ctx lval f args = lift_fun ctx (lift' ctx) S.threadenter ((|>) args % (|>) f % (|>) lval)
+  let threadspawn ctx lval f args fctx = lift_fun ctx (lift ctx) S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
+
+
+  let paths_as_set ctx =
+    let liftmap = List.map (fun x -> (x, snd ctx.local)) in
+    lift_fun ctx liftmap S.paths_as_set (Fun.id)
+
+  let event ctx e octx =
+    lift_fun ctx (lift ctx) S.event ((|>) (conv octx) % (|>) e)
+end
\ No newline at end of file
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 5de5b6f692..cacf48a912 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -22,6 +22,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
             (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
             |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)
             |> lift arg_enabled (module HashconsLifter)
+            |> lift true (module Delayed)
             |> lift arg_enabled (module WitnessConstraints.PathSensitive3)
             |> lift (not arg_enabled) (module PathSensitive2)
             |> lift (get_bool "ana.dead-code.branches") (module DeadBranchLifter)
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 074f501848..884e665209 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1045,6 +1045,12 @@
               "description": "Delay widenings using widening tokens.",
               "type": "boolean",
               "default": false
+            },
+            "delay": {
+              "title": "ana.widen.delay",
+              "description": "Delay widenings by count.",
+              "type": "integer",
+              "default": 0
             }
           },
           "additionalProperties": false
diff --git a/tests/regression/72-delayed/01-nontrivial.c b/tests/regression/72-delayed/01-nontrivial.c
new file mode 100644
index 0000000000..2c1f06bfd4
--- /dev/null
+++ b/tests/regression/72-delayed/01-nontrivial.c
@@ -0,0 +1,14 @@
+// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.widen.delay 1
+#include <goblint.h>
+extern _Bool __VERIFIER_nondet_bool();
+int main() {
+  int v = 0;
+  while (__VERIFIER_nondet_bool() == 0) {
+    __goblint_check(0 <= v);
+    __goblint_check(v <= 1);
+    if (v == 0)
+      v = 1;
+    // ...
+  }
+  return 0;
+}
\ No newline at end of file

From 786ed5de2189d98811d7fa80f047c9d099e2bb5d Mon Sep 17 00:00:00 2001
From: Ronald Judin <ronald.judin@ut.ee>
Date: Fri, 24 May 2024 11:43:35 +0300
Subject: [PATCH 02/12] Use delayed widening option in control.ml

---
 src/framework/control.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/framework/control.ml b/src/framework/control.ml
index cacf48a912..c921e8a52a 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -22,7 +22,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
             (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
             |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)
             |> lift arg_enabled (module HashconsLifter)
-            |> lift true (module Delayed)
+            |> lift (get_int "ana.widen.delay" > 0) (module Delayed)
             |> lift arg_enabled (module WitnessConstraints.PathSensitive3)
             |> lift (not arg_enabled) (module PathSensitive2)
             |> lift (get_bool "ana.dead-code.branches") (module DeadBranchLifter)

From b4863a565f2596fd0b35e8afd7d69a794a75d6a1 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 29 May 2024 11:52:32 +0300
Subject: [PATCH 03/12] Move widening delay lifter up to avoid crash with
 witness lifter

---
 src/framework/control.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/framework/control.ml b/src/framework/control.ml
index 44d43afa1c..6e76664f0a 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -25,10 +25,10 @@ let spec_module: (module Spec) Lazy.t = lazy (
       (module MCP.MCP2 : Spec)
       |> lift (get_int "ana.context.gas_value" >= 0) (module ContextGasLifter)
       |> lift true (module WidenContextLifterSide) (* option checked in functor *)
+      |> lift (get_int "ana.widen.delay" > 0) (module Delayed)
       (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
       |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)
       |> lift arg_enabled (module HashconsLifter)
-      |> lift (get_int "ana.widen.delay" > 0) (module Delayed)
       |> lift arg_enabled (module WitnessConstraints.PathSensitive3)
       |> lift (not arg_enabled) (module PathSensitive2)
       |> lift (get_bool "ana.dead-code.branches") (module DeadBranchLifter)

From e3a418662e18aa007b2118854f381a0e4c602f04 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 29 May 2024 12:02:13 +0300
Subject: [PATCH 04/12] Extract widening delay to separate module

---
 src/domain/lattice.ml        |  38 -----------
 src/framework/constraints.ml |  78 ----------------------
 src/framework/control.ml     |   2 +-
 src/goblint_lib.ml           |   2 +
 src/lifters/wideningDelay.ml | 125 +++++++++++++++++++++++++++++++++++
 5 files changed, 128 insertions(+), 117 deletions(-)
 create mode 100644 src/lifters/wideningDelay.ml

diff --git a/src/domain/lattice.ml b/src/domain/lattice.ml
index 09aea4fe99..99322c09d8 100644
--- a/src/domain/lattice.ml
+++ b/src/domain/lattice.ml
@@ -651,41 +651,3 @@ struct
   let pretty_diff () ((x:t),(y:t)): Pretty.doc =
     Pretty.dprintf "%a not leq %a" pretty x pretty y
 end
-
-module DelayedConf (C: Printable.ProdConfiguration) (Base: S) =
-struct
-  (** n () is an arbitrary constant *)
-  let n () = GobConfig.get_int "ana.widen.delay"
-  module P = (Printable.Chain (struct let n () = n () let names n = (string_of_int n) end))
-
-  include Printable.ProdConf (C) (Base) (P)
-
-  let bot () = (Base.bot (), 0)
-  let is_bot (b, _) = Base.is_bot b
-  let top () = (Base.top (), n ())
-  let is_top (b, _) = Base.is_top b
-
-  let leq (b1,_) (b2,_) = Base.leq b1 b2
-
-  let pretty_diff () (((b1,i1):t),((b2,i2):t)): Pretty.doc =
-    if Base.leq b1 b2 then
-      let f = fun () i -> Pretty.num i in
-      Pretty.dprintf "%a not leq %a" f i1 f i2
-    else
-      Base.pretty_diff () (b1,b2)
-
-  let join (b1,i1) (b2,i2) = (Base.join b1 b2, max i1 i2)
-  let meet (b1,i1) (b2,i2) = (Base.meet b1 b2, max i1 i2)
-  let narrow (b1,i1) (b2,i2) = (Base.narrow b1 b2, max i1 i2)
-  let widen (b1,i1) (b2,i2) =
-    if max i1 i2 < n () then
-      (Base.join b1 b2, 1 + max i1 i2)
-    else
-      (Base.widen b1 b2, max i1 i2)
-
-  let printXml f (b, i) =
-    BatPrintf.fprintf f "%a<analysis name=\"widen-delay\">%a</analysis>" Base.printXml b P.printXml i
-end
-
-module Delayed = DelayedConf (struct let expand_fst = true let expand_snd = true end)
-module DelayedSimple = DelayedConf (struct let expand_fst = false let expand_snd = false end)
\ No newline at end of file
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 9a1956a190..07180d54dd 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -2000,81 +2000,3 @@ struct
     Logs.info "Nodes comparison summary: %t" (fun () -> msg);
     Logs.newline ();
 end
-
-module Delayed (S:Spec)
-  : Spec with module D = Lattice.Delayed (S.D)
-          and module G = S.G
-          and module C = S.C
-=
-struct
-  module D = Lattice.Delayed (S.D)
-  module G = S.G
-  module C = S.C
-  module V = S.V
-  module P =
-  struct
-    include S.P
-    let of_elt (x, _) = of_elt x
-  end
-
-  let name () = S.name ()^" delayed"
-
-  let start_level = ref (`Top)
-
-  type marshal = S.marshal (* TODO: should hashcons table be in here to avoid relift altogether? *)
-  let init marshal =
-    S.init marshal
-
-  let finalize = S.finalize
-
-  let startstate v = (S.startstate v, 0)
-  let exitstate  v = (S.exitstate  v, D.n ())
-  let morphstate v (d,l) = (S.morphstate v d, l)
-
-  let conv (ctx: (D.t, G.t, C.t, V.t) ctx) : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
-    { ctx with local = fst ctx.local
-             ; split = (fun d es -> ctx.split (d, snd ctx.local) es )
-    }
-
-  let context ctx fd (d,_) = S.context (conv ctx) fd d
-  let startcontext () = S.startcontext ()
-
-  let lift_fun ctx f g h =
-    f @@ h (g (conv ctx))
-
-  let enter ctx r f args =
-    let liftmap = List.map (fun (x,y) -> (x, snd ctx.local), (y, snd ctx.local)) in
-    lift_fun ctx liftmap S.enter ((|>) args % (|>) f % (|>) r)
-
-  let lift ctx d = (d, 0)
-
-  (* Used only in the threadspawn function. *)
-  let rec lift' ctx dl =
-    match dl with
-    | [] -> []
-    | d::l -> (d, 0)::(lift' ctx l)
-
-  let sync ctx reason = lift_fun ctx (lift ctx) S.sync   ((|>) reason)
-  let query ctx (type a) (q: a Queries.t): a Queries.result = S.query (conv ctx) q
-  let assign ctx lv e = lift_fun ctx (lift ctx) S.assign ((|>) e % (|>) lv)
-  let vdecl ctx v     = lift_fun ctx (lift ctx) S.vdecl  ((|>) v)
-  let branch ctx e tv = lift_fun ctx (lift ctx) S.branch ((|>) tv % (|>) e)
-  let body ctx f      = lift_fun ctx (lift ctx) S.body   ((|>) f)
-  let return ctx r f  = lift_fun ctx (lift ctx) S.return ((|>) f % (|>) r)
-  let asm ctx         = lift_fun ctx (lift ctx) S.asm    identity
-  let skip ctx        = lift_fun ctx (lift ctx) S.skip identity
-  let special ctx r f args        = lift_fun ctx (lift ctx) S.special ((|>) args % (|>) f % (|>) r)
-  let combine_env ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_env (fun p -> p r fe f args fc (fst es) f_ask)
-  let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_assign (fun p -> p r fe f args fc (fst es) f_ask)
-
-  let threadenter ctx ~multiple lval f args = lift_fun ctx (lift' ctx) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval)
-  let threadspawn ctx ~multiple lval f args fctx = lift_fun ctx (lift ctx) (S.threadspawn ~multiple) ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
-
-
-  let paths_as_set ctx =
-    let liftmap = List.map (fun x -> (x, snd ctx.local)) in
-    lift_fun ctx liftmap S.paths_as_set (Fun.id)
-
-  let event ctx e octx =
-    lift_fun ctx (lift ctx) S.event ((|>) (conv octx) % (|>) e)
-end
\ No newline at end of file
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 6e76664f0a..dc1f480675 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -25,7 +25,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
       (module MCP.MCP2 : Spec)
       |> lift (get_int "ana.context.gas_value" >= 0) (module ContextGasLifter)
       |> lift true (module WidenContextLifterSide) (* option checked in functor *)
-      |> lift (get_int "ana.widen.delay" > 0) (module Delayed)
+      |> lift (get_int "ana.widen.delay" > 0) (module WideningDelay.Lifter)
       (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
       |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)
       |> lift arg_enabled (module HashconsLifter)
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 8013d9b2fe..104c0e0cbf 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -416,6 +416,8 @@ module ContextUtil = ContextUtil
 module ReturnUtil = ReturnUtil
 module BaseInvariant = BaseInvariant
 module CommonPriv = CommonPriv
+
+module WideningDelay = WideningDelay
 module WideningThresholds = WideningThresholds
 
 module VectorMatrix = VectorMatrix
diff --git a/src/lifters/wideningDelay.ml b/src/lifters/wideningDelay.ml
new file mode 100644
index 0000000000..173be3c60d
--- /dev/null
+++ b/src/lifters/wideningDelay.ml
@@ -0,0 +1,125 @@
+(** Standard widening delay with counters.
+
+    Abstract elements are paired with an integer counter, indicating how many times it has been widened.
+    Lifted abstract elements are only widened if the counter exceeds a predefined limit. *)
+
+open Batteries
+open Lattice
+open Analyses
+
+module DelayedConf (C: Printable.ProdConfiguration) (Base: S) =
+struct
+  (** n () is an arbitrary constant *)
+  let n () = GobConfig.get_int "ana.widen.delay"
+  module P = (Printable.Chain (struct let n () = n () let names n = (string_of_int n) end))
+
+  include Printable.ProdConf (C) (Base) (P)
+
+  let bot () = (Base.bot (), 0)
+  let is_bot (b, _) = Base.is_bot b
+  let top () = (Base.top (), n ())
+  let is_top (b, _) = Base.is_top b
+
+  let leq (b1,_) (b2,_) = Base.leq b1 b2
+
+  let pretty_diff () (((b1,i1):t),((b2,i2):t)): Pretty.doc =
+    if Base.leq b1 b2 then
+      let f = fun () i -> Pretty.num i in
+      Pretty.dprintf "%a not leq %a" f i1 f i2
+    else
+      Base.pretty_diff () (b1,b2)
+
+  let join (b1,i1) (b2,i2) = (Base.join b1 b2, max i1 i2)
+  let meet (b1,i1) (b2,i2) = (Base.meet b1 b2, max i1 i2)
+  let narrow (b1,i1) (b2,i2) = (Base.narrow b1 b2, max i1 i2)
+  let widen (b1,i1) (b2,i2) =
+    if max i1 i2 < n () then
+      (Base.join b1 b2, 1 + max i1 i2)
+    else
+      (Base.widen b1 b2, max i1 i2)
+
+  let printXml f (b, i) =
+    BatPrintf.fprintf f "%a<analysis name=\"widen-delay\">%a</analysis>" Base.printXml b P.printXml i
+end
+
+module Delayed = DelayedConf (struct let expand_fst = true let expand_snd = true end)
+module DelayedSimple = DelayedConf (struct let expand_fst = false let expand_snd = false end)
+
+
+module Lifter (S:Spec)
+  : Spec with module D = Delayed (S.D)
+          and module G = S.G
+          and module C = S.C
+=
+struct
+  module D = Delayed (S.D)
+  module G = S.G
+  module C = S.C
+  module V = S.V
+  module P =
+  struct
+    include S.P
+    let of_elt (x, _) = of_elt x
+  end
+
+  let name () = S.name ()^" delayed"
+
+  let start_level = ref (`Top)
+
+  type marshal = S.marshal (* TODO: should hashcons table be in here to avoid relift altogether? *)
+  let init marshal =
+    S.init marshal
+
+  let finalize = S.finalize
+
+  let startstate v = (S.startstate v, 0)
+  let exitstate  v = (S.exitstate  v, D.n ())
+  let morphstate v (d,l) = (S.morphstate v d, l)
+
+  let conv (ctx: (D.t, G.t, C.t, V.t) ctx) : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
+    { ctx with local = fst ctx.local
+             ; split = (fun d es -> ctx.split (d, snd ctx.local) es )
+    }
+
+  let context ctx fd (d,_) = S.context (conv ctx) fd d
+  let startcontext () = S.startcontext ()
+
+  let lift_fun ctx f g h =
+    f @@ h (g (conv ctx))
+
+  let enter ctx r f args =
+    let liftmap = List.map (fun (x,y) -> (x, snd ctx.local), (y, snd ctx.local)) in
+    lift_fun ctx liftmap S.enter ((|>) args % (|>) f % (|>) r)
+
+  let lift ctx d = (d, 0)
+
+  (* Used only in the threadspawn function. *)
+  let rec lift' ctx dl =
+    match dl with
+    | [] -> []
+    | d::l -> (d, 0)::(lift' ctx l)
+
+  let sync ctx reason = lift_fun ctx (lift ctx) S.sync   ((|>) reason)
+  let query ctx (type a) (q: a Queries.t): a Queries.result = S.query (conv ctx) q
+  let assign ctx lv e = lift_fun ctx (lift ctx) S.assign ((|>) e % (|>) lv)
+  let vdecl ctx v     = lift_fun ctx (lift ctx) S.vdecl  ((|>) v)
+  let branch ctx e tv = lift_fun ctx (lift ctx) S.branch ((|>) tv % (|>) e)
+  let body ctx f      = lift_fun ctx (lift ctx) S.body   ((|>) f)
+  let return ctx r f  = lift_fun ctx (lift ctx) S.return ((|>) f % (|>) r)
+  let asm ctx         = lift_fun ctx (lift ctx) S.asm    identity
+  let skip ctx        = lift_fun ctx (lift ctx) S.skip identity
+  let special ctx r f args        = lift_fun ctx (lift ctx) S.special ((|>) args % (|>) f % (|>) r)
+  let combine_env ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_env (fun p -> p r fe f args fc (fst es) f_ask)
+  let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_assign (fun p -> p r fe f args fc (fst es) f_ask)
+
+  let threadenter ctx ~multiple lval f args = lift_fun ctx (lift' ctx) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval)
+  let threadspawn ctx ~multiple lval f args fctx = lift_fun ctx (lift ctx) (S.threadspawn ~multiple) ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
+
+
+  let paths_as_set ctx =
+    let liftmap = List.map (fun x -> (x, snd ctx.local)) in
+    lift_fun ctx liftmap S.paths_as_set (Fun.id)
+
+  let event ctx e octx =
+    lift_fun ctx (lift ctx) S.event ((|>) (conv octx) % (|>) e)
+end
\ No newline at end of file

From 0ec39cfc713f80e83801d09237ccc98d0e00a6f6 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 29 May 2024 12:07:57 +0300
Subject: [PATCH 05/12] Reorganize analysis lifters

---
 src/goblint_lib.ml                      | 14 ++++++++++----
 src/{util => lifters}/wideningTokens.ml |  0
 2 files changed, 10 insertions(+), 4 deletions(-)
 rename src/{util => lifters}/wideningTokens.ml (100%)

diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 104c0e0cbf..b088d157fe 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -171,6 +171,16 @@ module AbortUnless = AbortUnless
 module PtranalAnalysis = PtranalAnalysis
 
 
+(** {1 Analysis lifters}
+
+    Transformations of analyses into extended analyses. *)
+
+module WideningDelay = WideningDelay
+module WideningTokens = WideningTokens
+
+module WitnessConstraints = WitnessConstraints
+
+
 (** {1 Domains}
 
     Domains used by analysis specifications and constraint systems are {{!Lattice.S} lattices}.
@@ -326,7 +336,6 @@ module WitnessUtil = WitnessUtil
     Automaton-based GraphML witnesses used in SV-COMP. *)
 
 module MyARG = MyARG
-module WitnessConstraints = WitnessConstraints
 module ArgTools = ArgTools
 module Witness = Witness
 module Graphml = Graphml
@@ -337,7 +346,6 @@ module Graphml = Graphml
 
 module YamlWitness = YamlWitness
 module YamlWitnessType = YamlWitnessType
-module WideningTokens = WideningTokens
 
 (** {3 Violation}
 
@@ -416,8 +424,6 @@ module ContextUtil = ContextUtil
 module ReturnUtil = ReturnUtil
 module BaseInvariant = BaseInvariant
 module CommonPriv = CommonPriv
-
-module WideningDelay = WideningDelay
 module WideningThresholds = WideningThresholds
 
 module VectorMatrix = VectorMatrix
diff --git a/src/util/wideningTokens.ml b/src/lifters/wideningTokens.ml
similarity index 100%
rename from src/util/wideningTokens.ml
rename to src/lifters/wideningTokens.ml

From db3e88dfd957be798ccf2e96fd3a78d4775c5110 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 29 May 2024 12:53:43 +0300
Subject: [PATCH 06/12] Refactor WideningDelay domain

---
 src/lifters/wideningDelay.ml | 59 ++++++++++++++++++------------------
 1 file changed, 30 insertions(+), 29 deletions(-)

diff --git a/src/lifters/wideningDelay.ml b/src/lifters/wideningDelay.ml
index 173be3c60d..453339a9fd 100644
--- a/src/lifters/wideningDelay.ml
+++ b/src/lifters/wideningDelay.ml
@@ -7,52 +7,53 @@ open Batteries
 open Lattice
 open Analyses
 
-module DelayedConf (C: Printable.ProdConfiguration) (Base: S) =
+module Dom (Base: S) =
 struct
-  (** n () is an arbitrary constant *)
-  let n () = GobConfig.get_int "ana.widen.delay"
-  module P = (Printable.Chain (struct let n () = n () let names n = (string_of_int n) end))
+  module ChainParams =
+  struct
+    let n () = GobConfig.get_int "ana.widen.delay"
+    let names = string_of_int
+  end
+  module Chain = Printable.Chain (ChainParams)
 
-  include Printable.ProdConf (C) (Base) (P)
+  include Printable.Prod (Base) (Chain)
 
   let bot () = (Base.bot (), 0)
   let is_bot (b, _) = Base.is_bot b
-  let top () = (Base.top (), n ())
+  let top () = (Base.top (), ChainParams.n ())
   let is_top (b, _) = Base.is_top b
 
-  let leq (b1,_) (b2,_) = Base.leq b1 b2
+  let leq (b1, _) (b2, _) = Base.leq b1 b2
 
-  let pretty_diff () (((b1,i1):t),((b2,i2):t)): Pretty.doc =
-    if Base.leq b1 b2 then
-      let f = fun () i -> Pretty.num i in
-      Pretty.dprintf "%a not leq %a" f i1 f i2
+  (** All operations keep maximal counter. *)
+  let join (b1, i1) (b2, i2) = (Base.join b1 b2, max i1 i2)
+  let meet (b1, i1) (b2, i2) = (Base.meet b1 b2, max i1 i2)
+  let widen (b1, i1) (b2, i2) =
+    let i' = max i1 i2 in
+    if i' < ChainParams.n () then
+      (Base.join b1 b2, i' + 1)
     else
-      Base.pretty_diff () (b1,b2)
-
-  let join (b1,i1) (b2,i2) = (Base.join b1 b2, max i1 i2)
-  let meet (b1,i1) (b2,i2) = (Base.meet b1 b2, max i1 i2)
-  let narrow (b1,i1) (b2,i2) = (Base.narrow b1 b2, max i1 i2)
-  let widen (b1,i1) (b2,i2) =
-    if max i1 i2 < n () then
-      (Base.join b1 b2, 1 + max i1 i2)
-    else
-      (Base.widen b1 b2, max i1 i2)
+      (Base.widen b1 b2, i') (* Don't increase beyond n, otherwise TD3 will not reach fixpoint w.r.t. equal. *)
+  let narrow (b1, i1) (b2, i2) = (Base.narrow b1 b2, max i1 i2)
 
-  let printXml f (b, i) =
-    BatPrintf.fprintf f "%a<analysis name=\"widen-delay\">%a</analysis>" Base.printXml b P.printXml i
+  let pretty_diff () ((b1, _), (b2, _)) =
+    Base.pretty_diff () (b1, b2) (* Counters cannot violate leq. *)
 end
 
-module Delayed = DelayedConf (struct let expand_fst = true let expand_snd = true end)
-module DelayedSimple = DelayedConf (struct let expand_fst = false let expand_snd = false end)
-
 
 module Lifter (S:Spec)
-  : Spec with module D = Delayed (S.D)
+  : Spec with module D = Dom (S.D)
           and module G = S.G
           and module C = S.C
 =
 struct
-  module D = Delayed (S.D)
+  module D =
+  struct
+    include Dom (S.D)
+
+    let printXml f (b, i) =
+      BatPrintf.fprintf f "%a<analysis name=\"widen-delay\">%a</analysis>" S.D.printXml b Chain.printXml i
+  end
   module G = S.G
   module C = S.C
   module V = S.V
@@ -73,7 +74,7 @@ struct
   let finalize = S.finalize
 
   let startstate v = (S.startstate v, 0)
-  let exitstate  v = (S.exitstate  v, D.n ())
+  let exitstate  v = (S.exitstate  v, D.ChainParams.n ())
   let morphstate v (d,l) = (S.morphstate v d, l)
 
   let conv (ctx: (D.t, G.t, C.t, V.t) ctx) : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =

From 2557f7de320e5c16b14fb31d819080a764a7dc60 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 29 May 2024 13:03:17 +0300
Subject: [PATCH 07/12] Clean up WideningDelay lifter

---
 src/lifters/wideningDelay.ml | 71 ++++++++++++++----------------------
 1 file changed, 28 insertions(+), 43 deletions(-)

diff --git a/src/lifters/wideningDelay.ml b/src/lifters/wideningDelay.ml
index 453339a9fd..cd17bebaf9 100644
--- a/src/lifters/wideningDelay.ml
+++ b/src/lifters/wideningDelay.ml
@@ -41,11 +41,7 @@ struct
 end
 
 
-module Lifter (S:Spec)
-  : Spec with module D = Dom (S.D)
-          and module G = S.G
-          and module C = S.C
-=
+module Lifter (S: Spec): Spec =
 struct
   module D =
   struct
@@ -63,64 +59,53 @@ struct
     let of_elt (x, _) = of_elt x
   end
 
-  let name () = S.name ()^" delayed"
-
-  let start_level = ref (`Top)
-
-  type marshal = S.marshal (* TODO: should hashcons table be in here to avoid relift altogether? *)
-  let init marshal =
-    S.init marshal
+  let name () = S.name () ^ " with widening delay"
 
+  type marshal = S.marshal
+  let init = S.init
   let finalize = S.finalize
 
   let startstate v = (S.startstate v, 0)
-  let exitstate  v = (S.exitstate  v, D.ChainParams.n ())
-  let morphstate v (d,l) = (S.morphstate v d, l)
+  let exitstate  v = (S.exitstate  v, 0)
+  let morphstate v (d, l) = (S.morphstate v d, l)
 
-  let conv (ctx: (D.t, G.t, C.t, V.t) ctx) : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
+  let conv (ctx: (D.t, G.t, C.t, V.t) ctx): (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
     { ctx with local = fst ctx.local
-             ; split = (fun d es -> ctx.split (d, snd ctx.local) es )
+             ; split = (fun d es -> ctx.split (d, 0) es)
     }
 
-  let context ctx fd (d,_) = S.context (conv ctx) fd d
+  let context ctx fd (d, _) = S.context (conv ctx) fd d
   let startcontext () = S.startcontext ()
 
   let lift_fun ctx f g h =
     f @@ h (g (conv ctx))
 
-  let enter ctx r f args =
-    let liftmap = List.map (fun (x,y) -> (x, snd ctx.local), (y, snd ctx.local)) in
-    lift_fun ctx liftmap S.enter ((|>) args % (|>) f % (|>) r)
-
-  let lift ctx d = (d, 0)
-
-  (* Used only in the threadspawn function. *)
-  let rec lift' ctx dl =
-    match dl with
-    | [] -> []
-    | d::l -> (d, 0)::(lift' ctx l)
+  let lift d = (d, 0)
 
-  let sync ctx reason = lift_fun ctx (lift ctx) S.sync   ((|>) reason)
+  let sync ctx reason = lift_fun ctx lift S.sync   ((|>) reason)
   let query ctx (type a) (q: a Queries.t): a Queries.result = S.query (conv ctx) q
-  let assign ctx lv e = lift_fun ctx (lift ctx) S.assign ((|>) e % (|>) lv)
-  let vdecl ctx v     = lift_fun ctx (lift ctx) S.vdecl  ((|>) v)
-  let branch ctx e tv = lift_fun ctx (lift ctx) S.branch ((|>) tv % (|>) e)
-  let body ctx f      = lift_fun ctx (lift ctx) S.body   ((|>) f)
-  let return ctx r f  = lift_fun ctx (lift ctx) S.return ((|>) f % (|>) r)
-  let asm ctx         = lift_fun ctx (lift ctx) S.asm    identity
-  let skip ctx        = lift_fun ctx (lift ctx) S.skip identity
-  let special ctx r f args        = lift_fun ctx (lift ctx) S.special ((|>) args % (|>) f % (|>) r)
-  let combine_env ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_env (fun p -> p r fe f args fc (fst es) f_ask)
-  let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_assign (fun p -> p r fe f args fc (fst es) f_ask)
+  let assign ctx lv e = lift_fun ctx lift S.assign ((|>) e % (|>) lv)
+  let vdecl ctx v     = lift_fun ctx lift S.vdecl  ((|>) v)
+  let branch ctx e tv = lift_fun ctx lift S.branch ((|>) tv % (|>) e)
+  let body ctx f      = lift_fun ctx lift S.body   ((|>) f)
+  let return ctx r f  = lift_fun ctx lift S.return ((|>) f % (|>) r)
+  let asm ctx         = lift_fun ctx lift S.asm    identity
+  let skip ctx        = lift_fun ctx lift S.skip identity
+  let special ctx r f args = lift_fun ctx lift S.special ((|>) args % (|>) f % (|>) r)
 
-  let threadenter ctx ~multiple lval f args = lift_fun ctx (lift' ctx) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval)
-  let threadspawn ctx ~multiple lval f args fctx = lift_fun ctx (lift ctx) (S.threadspawn ~multiple) ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
+  let enter ctx r f args =
+    let liftmap = List.map (Tuple2.mapn lift) in
+    lift_fun ctx liftmap S.enter ((|>) args % (|>) f % (|>) r)
+  let combine_env ctx r fe f args fc es f_ask = lift_fun ctx lift S.combine_env (fun p -> p r fe f args fc (fst es) f_ask)
+  let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx lift S.combine_assign (fun p -> p r fe f args fc (fst es) f_ask)
 
+  let threadenter ctx ~multiple lval f args = lift_fun ctx (List.map lift) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval)
+  let threadspawn ctx ~multiple lval f args fctx = lift_fun ctx lift (S.threadspawn ~multiple) ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
 
   let paths_as_set ctx =
     let liftmap = List.map (fun x -> (x, snd ctx.local)) in
-    lift_fun ctx liftmap S.paths_as_set (Fun.id)
+    lift_fun ctx liftmap S.paths_as_set Fun.id
 
   let event ctx e octx =
-    lift_fun ctx (lift ctx) S.event ((|>) (conv octx) % (|>) e)
+    lift_fun ctx lift S.event ((|>) (conv octx) % (|>) e)
 end
\ No newline at end of file

From 766019e3e4107ed6949b1e19609329089d72d946 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 29 May 2024 13:15:47 +0300
Subject: [PATCH 08/12] Add widening delay example

---
 ...ivial.c => 01-mine-tutorial-ex4.8-delay.c} |  2 +-
 .../82-widen/02-mihaila-widen-fig7-delay.c    | 20 +++++++++++++++++++
 2 files changed, 21 insertions(+), 1 deletion(-)
 rename tests/regression/82-widen/{01-widen-delay-nontrivial.c => 01-mine-tutorial-ex4.8-delay.c} (99%)
 create mode 100644 tests/regression/82-widen/02-mihaila-widen-fig7-delay.c

diff --git a/tests/regression/82-widen/01-widen-delay-nontrivial.c b/tests/regression/82-widen/01-mine-tutorial-ex4.8-delay.c
similarity index 99%
rename from tests/regression/82-widen/01-widen-delay-nontrivial.c
rename to tests/regression/82-widen/01-mine-tutorial-ex4.8-delay.c
index 2c1f06bfd4..3b9e82b277 100644
--- a/tests/regression/82-widen/01-widen-delay-nontrivial.c
+++ b/tests/regression/82-widen/01-mine-tutorial-ex4.8-delay.c
@@ -11,4 +11,4 @@ int main() {
     // ...
   }
   return 0;
-}
\ No newline at end of file
+}
diff --git a/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c b/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c
new file mode 100644
index 0000000000..e5890a80a2
--- /dev/null
+++ b/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c
@@ -0,0 +1,20 @@
+// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.widen.delay 3
+// From "Widening as Abstract Domain", Fig. 7: https://doi.org/10.1007/978-3-642-38088-4_12
+// They claim delay 2 (https://bytebucket.org/mihaila/bindead/wiki/resources/widening-talk.pdf), we need 3 for some reason. Why?
+#include <goblint.h>
+extern _Bool __VERIFIER_nondet_bool();
+
+int main() {
+  int x = 0;
+  int y = 0;
+  while (x < 100) {
+    __goblint_check(0 <= y);
+    __goblint_check(y <= 1);
+    if (__VERIFIER_nondet_bool())
+      y = 1;
+    x = x + 4;
+  }
+  __goblint_check(0 <= y);
+  __goblint_check(y <= 1);
+  return 0;
+}

From d8d665b8ba0c33a30960dd44085e055b8fcf81e5 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 29 May 2024 13:35:26 +0300
Subject: [PATCH 09/12] Implement global widening delay

---
 src/config/options.schema.json                | 19 +++-
 src/framework/control.ml                      |  3 +-
 src/lifters/wideningDelay.ml                  | 90 ++++++++++++++++---
 .../82-widen/01-mine-tutorial-ex4.8-delay.c   |  2 +-
 .../82-widen/02-mihaila-widen-fig7-delay.c    |  2 +-
 tests/regression/82-widen/03-mine14-delay.c   | 35 ++++++++
 6 files changed, 135 insertions(+), 16 deletions(-)
 create mode 100644 tests/regression/82-widen/03-mine14-delay.c

diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index 3c00660c81..bf2df2f20e 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -1129,9 +1129,22 @@
             },
             "delay": {
               "title": "ana.widen.delay",
-              "description": "Delay widenings by count.",
-              "type": "integer",
-              "default": 0
+              "type": "object",
+              "properties": {
+                "local": {
+                  "title": "ana.widen.delay.local",
+                  "description": "Delay local widenings by count.",
+                  "type": "integer",
+                  "default": 0
+                },
+                "global": {
+                  "title": "ana.widen.delay.global",
+                  "description": "Delay global widenings by count.",
+                  "type": "integer",
+                  "default": 0
+                }
+              },
+              "additionalProperties": false
             }
           },
           "additionalProperties": false
diff --git a/src/framework/control.ml b/src/framework/control.ml
index dc1f480675..18130b1aed 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -25,7 +25,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
       (module MCP.MCP2 : Spec)
       |> lift (get_int "ana.context.gas_value" >= 0) (module ContextGasLifter)
       |> lift true (module WidenContextLifterSide) (* option checked in functor *)
-      |> lift (get_int "ana.widen.delay" > 0) (module WideningDelay.Lifter)
+      |> lift (get_int "ana.widen.delay.local" > 0) (module WideningDelay.DLifter)
       (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
       |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)
       |> lift arg_enabled (module HashconsLifter)
@@ -42,6 +42,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
       |> lift (get_bool "ana.widen.tokens") (module WideningTokens.Lifter)
       |> lift true (module LongjmpLifter)
       |> lift termination_enabled (module RecursionTermLifter) (* Always activate the recursion termination analysis, when the loop termination analysis is activated*)
+      |> lift (get_int "ana.widen.delay.global" > 0) (module WideningDelay.GLifter)
     )
   in
   GobConfig.building_spec := false;
diff --git a/src/lifters/wideningDelay.ml b/src/lifters/wideningDelay.ml
index cd17bebaf9..1cc8585935 100644
--- a/src/lifters/wideningDelay.ml
+++ b/src/lifters/wideningDelay.ml
@@ -7,15 +7,21 @@ open Batteries
 open Lattice
 open Analyses
 
-module Dom (Base: S) =
+module LocalChainParams: Printable.ChainParams =
 struct
-  module ChainParams =
-  struct
-    let n () = GobConfig.get_int "ana.widen.delay"
-    let names = string_of_int
-  end
-  module Chain = Printable.Chain (ChainParams)
+  let n () = GobConfig.get_int "ana.widen.delay.local"
+  let names = string_of_int
+end
 
+module GlobalChainParams: Printable.ChainParams =
+struct
+  let n () = GobConfig.get_int "ana.widen.delay.global"
+  let names = string_of_int
+end
+
+module Dom (Base: S) (ChainParams: Printable.ChainParams) =
+struct
+  module Chain = Printable.Chain (ChainParams)
   include Printable.Prod (Base) (Chain)
 
   let bot () = (Base.bot (), 0)
@@ -41,11 +47,11 @@ struct
 end
 
 
-module Lifter (S: Spec): Spec =
+module DLifter (S: Spec): Spec =
 struct
   module D =
   struct
-    include Dom (S.D)
+    include Dom (S.D) (LocalChainParams)
 
     let printXml f (b, i) =
       BatPrintf.fprintf f "%a<analysis name=\"widen-delay\">%a</analysis>" S.D.printXml b Chain.printXml i
@@ -108,4 +114,68 @@ struct
 
   let event ctx e octx =
     lift_fun ctx lift S.event ((|>) (conv octx) % (|>) e)
-end
\ No newline at end of file
+end
+
+module GLifter (S: Spec): Spec =
+struct
+  module D = S.D
+  module G =
+  struct
+    include Dom (S.G) (GlobalChainParams)
+
+    let printXml f (b, i) =
+      BatPrintf.fprintf f "%a<analysis name=\"widen-delay\">%a</analysis>" S.G.printXml b Chain.printXml i
+  end
+  module C = S.C
+  module V = S.V
+  module P = S.P
+
+  let name () = S.name () ^ " with widening delay"
+
+  type marshal = S.marshal
+  let init = S.init
+  let finalize = S.finalize
+
+  let startstate v = S.startstate v
+  let exitstate  v = S.exitstate  v
+  let morphstate v d = S.morphstate v d
+
+  let conv (ctx: (D.t, G.t, C.t, V.t) ctx): (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
+    { ctx with global = (fun v -> fst (ctx.global v))
+             ; sideg = (fun v g -> ctx.sideg v (g, 0))
+    }
+
+  let context ctx fd d = S.context (conv ctx) fd d
+  let startcontext () = S.startcontext ()
+
+  let lift_fun ctx f g h =
+    f @@ h (g (conv ctx))
+
+  let lift d = d
+
+  let sync ctx reason = lift_fun ctx lift S.sync   ((|>) reason)
+  let query ctx (type a) (q: a Queries.t): a Queries.result = S.query (conv ctx) q
+  let assign ctx lv e = lift_fun ctx lift S.assign ((|>) e % (|>) lv)
+  let vdecl ctx v     = lift_fun ctx lift S.vdecl  ((|>) v)
+  let branch ctx e tv = lift_fun ctx lift S.branch ((|>) tv % (|>) e)
+  let body ctx f      = lift_fun ctx lift S.body   ((|>) f)
+  let return ctx r f  = lift_fun ctx lift S.return ((|>) f % (|>) r)
+  let asm ctx         = lift_fun ctx lift S.asm    identity
+  let skip ctx        = lift_fun ctx lift S.skip identity
+  let special ctx r f args = lift_fun ctx lift S.special ((|>) args % (|>) f % (|>) r)
+
+  let enter ctx r f args =
+    let liftmap = List.map (Tuple2.mapn lift) in
+    lift_fun ctx liftmap S.enter ((|>) args % (|>) f % (|>) r)
+  let combine_env ctx r fe f args fc es f_ask = lift_fun ctx lift S.combine_env (fun p -> p r fe f args fc es f_ask)
+  let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx lift S.combine_assign (fun p -> p r fe f args fc es f_ask)
+
+  let threadenter ctx ~multiple lval f args = lift_fun ctx (List.map lift) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval)
+  let threadspawn ctx ~multiple lval f args fctx = lift_fun ctx lift (S.threadspawn ~multiple) ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
+
+  let paths_as_set ctx =
+    lift_fun ctx Fun.id S.paths_as_set Fun.id
+
+  let event ctx e octx =
+    lift_fun ctx lift S.event ((|>) (conv octx) % (|>) e)
+end
diff --git a/tests/regression/82-widen/01-mine-tutorial-ex4.8-delay.c b/tests/regression/82-widen/01-mine-tutorial-ex4.8-delay.c
index 3b9e82b277..d6fb982b82 100644
--- a/tests/regression/82-widen/01-mine-tutorial-ex4.8-delay.c
+++ b/tests/regression/82-widen/01-mine-tutorial-ex4.8-delay.c
@@ -1,4 +1,4 @@
-// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.widen.delay 1
+// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.widen.delay.local 1
 #include <goblint.h>
 extern _Bool __VERIFIER_nondet_bool();
 int main() {
diff --git a/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c b/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c
index e5890a80a2..375308851b 100644
--- a/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c
+++ b/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c
@@ -1,4 +1,4 @@
-// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.widen.delay 3
+// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.widen.delay.local 3
 // From "Widening as Abstract Domain", Fig. 7: https://doi.org/10.1007/978-3-642-38088-4_12
 // They claim delay 2 (https://bytebucket.org/mihaila/bindead/wiki/resources/widening-talk.pdf), we need 3 for some reason. Why?
 #include <goblint.h>
diff --git a/tests/regression/82-widen/03-mine14-delay.c b/tests/regression/82-widen/03-mine14-delay.c
new file mode 100644
index 0000000000..433bd19d7e
--- /dev/null
+++ b/tests/regression/82-widen/03-mine14-delay.c
@@ -0,0 +1,35 @@
+// PARAM: --set ana.path_sens[+] threadflag --set ana.base.privatization mutex-meet-tid --enable ana.int.interval --set ana.widen.delay.local 100 --set ana.widen.delay.global 100
+// Fig 5a from Miné 2014
+#include <pthread.h>
+#include <stdio.h>
+#include <goblint.h>
+
+int x;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  int top;
+  while(top) {
+    pthread_mutex_lock(&mutex);
+    if(x<100) {
+      x++;
+    }
+    pthread_mutex_unlock(&mutex);
+  }
+  return NULL;
+}
+
+
+int main(void) {
+  int top, top2;
+
+
+  pthread_t id;
+  pthread_t id2;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_create(&id2, NULL, t_fun, NULL);
+  pthread_mutex_lock(&mutex);
+  __goblint_check(x <= 100);
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}

From f34fc1406d52d7155293ebac1607b247d4db709a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 30 May 2024 11:11:19 +0300
Subject: [PATCH 10/12] Add comment about widening delay transfer functions

---
 src/lifters/wideningDelay.ml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/lifters/wideningDelay.ml b/src/lifters/wideningDelay.ml
index 1cc8585935..8bd0135167 100644
--- a/src/lifters/wideningDelay.ml
+++ b/src/lifters/wideningDelay.ml
@@ -47,6 +47,9 @@ struct
 end
 
 
+(** Lift {!S} to use widening delay for local states.
+
+    All transfer functions reset the counter to 0, so counting only happens between old and new values at a local unknown. *)
 module DLifter (S: Spec): Spec =
 struct
   module D =
@@ -116,6 +119,7 @@ struct
     lift_fun ctx lift S.event ((|>) (conv octx) % (|>) e)
 end
 
+(** Lift {!S} to use widening delay for global unknowns. *)
 module GLifter (S: Spec): Spec =
 struct
   module D = S.D

From 1a8021defafe10f1ad8eca82b773efe5947e19f7 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 7 Jun 2024 15:44:43 +0300
Subject: [PATCH 11/12] Split 82-widen/02-mihaila-widen-fig7-delay into two
 tests

---
 .../82-widen/02-mihaila-widen-fig7-delay.c    |  3 +--
 .../82-widen/03-mihaila-widen-slide-delay.c   | 19 +++++++++++++++++++
 .../{03-mine14-delay.c => 04-mine14-delay.c}  |  0
 3 files changed, 20 insertions(+), 2 deletions(-)
 create mode 100644 tests/regression/82-widen/03-mihaila-widen-slide-delay.c
 rename tests/regression/82-widen/{03-mine14-delay.c => 04-mine14-delay.c} (100%)

diff --git a/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c b/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c
index 375308851b..4106bf985d 100644
--- a/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c
+++ b/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c
@@ -1,6 +1,5 @@
-// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.widen.delay.local 3
+// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.widen.delay.local 1
 // From "Widening as Abstract Domain", Fig. 7: https://doi.org/10.1007/978-3-642-38088-4_12
-// They claim delay 2 (https://bytebucket.org/mihaila/bindead/wiki/resources/widening-talk.pdf), we need 3 for some reason. Why?
 #include <goblint.h>
 extern _Bool __VERIFIER_nondet_bool();
 
diff --git a/tests/regression/82-widen/03-mihaila-widen-slide-delay.c b/tests/regression/82-widen/03-mihaila-widen-slide-delay.c
new file mode 100644
index 0000000000..5f511e1a4c
--- /dev/null
+++ b/tests/regression/82-widen/03-mihaila-widen-slide-delay.c
@@ -0,0 +1,19 @@
+// PARAM: --disable ana.int.def_exc --enable ana.int.interval --set ana.widen.delay.local 3
+// From "Widening as Abstract Domain" slides: https://bytebucket.org/mihaila/bindead/wiki/resources/widening-talk.pdf
+// They claim delay 2, we need 3 for some reason. Why?
+#include <goblint.h>
+
+int main() {
+  int x = 0;
+  int y = 0;
+  while (x < 100) {
+    __goblint_check(0 <= y);
+    __goblint_check(y <= 1);
+    if (x > 5)
+      y = 1;
+    x = x + 4;
+  }
+  __goblint_check(0 <= y);
+  __goblint_check(y <= 1);
+  return 0;
+}
diff --git a/tests/regression/82-widen/03-mine14-delay.c b/tests/regression/82-widen/04-mine14-delay.c
similarity index 100%
rename from tests/regression/82-widen/03-mine14-delay.c
rename to tests/regression/82-widen/04-mine14-delay.c

From 2eca6d6488d94052bc77c43a0afab582c04c2aa0 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 7 Jun 2024 15:57:58 +0300
Subject: [PATCH 12/12] Explain 82-widen/03-mihaila-widen-slide-delay

---
 tests/regression/82-widen/02-mihaila-widen-fig7-delay.c  | 5 +++++
 tests/regression/82-widen/03-mihaila-widen-slide-delay.c | 8 +++++++-
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c b/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c
index 4106bf985d..e0d908ff69 100644
--- a/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c
+++ b/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c
@@ -1,5 +1,10 @@
 // PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.widen.delay.local 1
 // From "Widening as Abstract Domain", Fig. 7: https://doi.org/10.1007/978-3-642-38088-4_12
+// Delay 1:
+// 0. {x -> [0,0], y -> [0,0]}
+// 1. {x -> [0,4], y -> [0,1]} (delay 0 would widen already here)
+// 2. {x -> [0,+inf], y -> [0,1]}
+// narrow: {x -> [0,103], y -> [0,1]}
 #include <goblint.h>
 extern _Bool __VERIFIER_nondet_bool();
 
diff --git a/tests/regression/82-widen/03-mihaila-widen-slide-delay.c b/tests/regression/82-widen/03-mihaila-widen-slide-delay.c
index 5f511e1a4c..720bcb04d0 100644
--- a/tests/regression/82-widen/03-mihaila-widen-slide-delay.c
+++ b/tests/regression/82-widen/03-mihaila-widen-slide-delay.c
@@ -1,6 +1,12 @@
 // PARAM: --disable ana.int.def_exc --enable ana.int.interval --set ana.widen.delay.local 3
 // From "Widening as Abstract Domain" slides: https://bytebucket.org/mihaila/bindead/wiki/resources/widening-talk.pdf
-// They claim delay 2, we need 3 for some reason. Why?
+// They claim delay 2, we need 3:
+// 0. {x -> [0,0], y -> [0,0]}
+// 1. {x -> [0,4], y -> [0,0]}
+// 2. {x -> [0,8], y -> [0,0]}
+// 3. {x -> [0,12], y -> [0,1]} (delay 2 would widen already here)
+// 4. {x -> [0,+inf], y -> [0,1]}
+// narrow: {x -> [0,103], y -> [0,1]}
 #include <goblint.h>
 
 int main() {