diff --git a/dune-project b/dune-project
index aabe7b4243..05ec842402 100644
--- a/dune-project
+++ b/dune-project
@@ -69,6 +69,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
     conf-gcc ; ensures opam-repository CI installs real gcc from homebrew on MacOS
     domain-local-await
     domain_shims
+    ocplib-simplex
   )
   (depopts
     apron
diff --git a/goblint.opam b/goblint.opam
index b7d956738c..0c892712ff 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -71,6 +71,7 @@ depends: [
   "conf-gcc"
   "domain-local-await"
   "domain_shims"
+  "ocplib-simplex"
 ]
 depopts: ["apron" "z3" "domainslib"]
 conflicts: [
diff --git a/goblint.opam.locked b/goblint.opam.locked
index 78384eb649..f0c527d2c4 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -84,6 +84,7 @@ depends: [
   "ocaml-variants" {= "4.14.2+options"}
   "ocamlbuild" {= "0.14.3"}
   "ocamlfind" {= "1.9.8"}
+  "ocplib-simplex" {= "0.5.1"}
   "odoc" {= "3.0.0" & with-doc}
   "odoc-parser" {= "3.0.0" & with-doc}
   "ordering" {= "3.19.1"}
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index 5d66659b43..09242577c1 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -76,7 +76,7 @@ struct
             if VH.mem v_ins v then
               VH.find v_ins v
             else
-              let v_in = Cilfacade.create_var @@ makeVarinfo false (v.vname ^ "#in") v.vtype in (* temporary local g#in for global g *)
+              let v_in = Cilfacade.create_var @@ makeVarinfo false (v.vname ^  "#in") v.vtype in (* temporary local g#in for global g *)
               v_in.vattr <- v.vattr; (* preserve goblint_relation_track attribute *)
               VH.replace v_ins v v_in;
               v_in
@@ -628,6 +628,8 @@ struct
     else
       Invariant.none
 
+  let query_my_invariant man = MyInvariant.of_lincons1_set (RD.invariant_set man.local.rel)
+
   let query man (type a) (q: a Queries.t): a Queries.result =
     let open Queries in
     let st = man.local in
@@ -652,6 +654,7 @@ struct
     | Queries.InvariantGlobal g ->
       let g: V.t = Obj.obj g in
       query_invariant_global man g
+    | Queries.MyInvariant _ -> query_my_invariant man
     | _ -> Result.top q
 
 
diff --git a/src/analyses/loopTermination.ml b/src/analyses/loopTermination.ml
index 69251f058f..1b8a9eda6b 100644
--- a/src/analyses/loopTermination.ml
+++ b/src/analyses/loopTermination.ml
@@ -5,10 +5,328 @@
 open Analyses
 open GoblintCil
 open TerminationPreprocessing
+open ListMatrix
+open SparseVector
+open GobApron
 
 (** Contains all loop counter variables (varinfo) and maps them to their corresponding loop statement. *)
 let loop_counters : stmt VarToStmt.t ref = ref VarToStmt.empty
 
+module V = struct
+  type t = string
+  let is_int _ = true
+  let compare = String.compare
+  let print fmt v = Format.fprintf fmt "%s" v
+end
+
+module Rat = struct
+  include Mpqf
+  let zero = of_int 0
+  let one = of_int 1
+  let m_one = of_int (-1)
+  let is_zero x = cmp_int x 0 = 0
+  let is_one x = cmp_int x 1 = 0
+  let is_m_one x = cmp_int x (-1) = 0
+  let is_int x = is_one (of_mpz (get_den x)) (* I assume the numbers to be normalized *)
+  let min x y = if cmp x y <= 0 then x else y
+  let floor x =
+    let n = get_num x in
+    let d = get_den x in
+    of_mpz (Mpzf.fdiv_q n d)
+  let ceiling x =
+    let n = get_num x in
+    let d = get_den x in
+    of_mpz (Mpzf.cdiv_q n d)
+  let minus = neg
+  let sign = sgn
+  let compare = cmp
+  let mult = mul
+  let hash _ = 0
+  let get_den x = Z.of_string (Mpzf.to_string (get_den x))
+  let get_num x = Z.of_string (Mpzf.to_string (get_num x))
+end
+
+module Ex = struct
+  include Set.Make(String)
+
+  let print fmt s = match elements s with
+    | [] -> Format.fprintf fmt "()"
+    | e::l ->
+      Format.fprintf fmt "%s" e;
+      List.iter (Format.fprintf fmt ", %s") l
+end
+
+module Sim = OcplibSimplex.Basic.Make (V) (Rat) (Ex)
+
+module Matrix = ListMatrix (Rat) (SparseVector)
+
+module SparseVec = SparseVector (Rat)
+
+module StringSet = Set.Make (String)
+
+let string_of_invariant (constraints: Invariant.t) =
+  match constraints with
+  | `Top -> "Top"
+  | `Bot -> "Bot"
+  | `Lifted constraints -> constraints |> Invariant.Exp.process |> List.map Invariant.Exp.show |> String.concat "; "
+
+let exp_list_of_constraints (constraints : Invariant.t) =
+  match constraints with
+  | `Top -> []
+  | `Bot -> failwith "Constraints are Bot"
+  | `Lifted cs ->
+    (* Split Eq into two Le's and mirror Ge into Le *)
+    let to_leq acc = function
+      | BinOp (Le, _, _, _) as e -> e :: acc
+      | BinOp (Ge, e1, e2, t) -> (BinOp (Le, e2, e1, t)) :: acc
+      | BinOp (Eq, e1, e2, t) -> (BinOp (Le, e1, e2, t)) :: (BinOp (Le, e2, e1, t)) :: acc
+      | BinOp (Ne, _, _, _) -> acc
+      | _ -> failwith "Found something else" in
+    let cs =
+      cs |> Invariant.Exp.process |> List.map Invariant.Exp.to_cil |> List.fold_left to_leq []
+    in
+    if M.tracing then
+      (M.trace "termination" "Constraints: %s" (string_of_invariant constraints);
+       M.trace "termination" "Number of constraints after conversion to Leq list: %i" (List.length cs));
+    cs
+
+let coeff_in_exp vname e =
+  let rec inner = function
+    | BinOp (PlusA, e1, e2, _) ->
+      (match inner e1, inner e2 with
+       | Some c1, Some c2 -> failwith "This shouldn't happen"
+       | None, None -> None
+       | c, None | None, c -> c)
+    | BinOp (MinusA, e1, e2, _) ->
+      failwith "found a Minus"
+    | BinOp (Mult, Const (CInt (c, _, _)), Lval (Var v, _), _) -> if v.vname = vname then Some (c |> cilint_to_int |> Rat.of_int) else None
+    | BinOp (Mult, _, _, _) -> failwith "found another Mult"
+    | Const (CInt (c, _, _)) -> None
+    | Lval (Var v, _) -> if v.vname = vname then Some Rat.one else None
+    | BinOp (Mod, _, _, _) -> None
+    | _ -> failwith "found something unexpected"
+  in
+  match e with
+  | BinOp (Le, e1, e2, _) ->
+    (match inner e1, inner e2 with
+     | Some c1, Some c2 -> failwith "This shouldn't happen"
+     | None, None -> Rat.zero
+     | Some c, None -> c
+     | None, Some c -> Rat.neg c)
+  | _ -> failwith "This shouldn't happen"
+
+let get_var vname env =
+  let vars, _ = Environment.vars env in
+  Array.find_map (fun v -> if Var.to_string v = vname then Some v else None) vars
+
+let coeff_in_lincons1 vname (e: Lincons1.t) =
+  match get_var vname e.env with
+  | None -> Rat.zero
+  | Some v ->
+    match Lincons1.get_coeff e v with
+    | Interval _ -> failwith "Lincons1 coeff is an interval, this shouldn't happen"
+    | Scalar s ->
+      s |> SharedFunctions.int_of_scalar |> Option.get |> Z.to_int |> Rat.of_int |> Rat.minus (* negate the coefficient because of SUPEQ typ *)
+
+let const_in_exp e =
+  let rec inner = function
+    | BinOp (PlusA, e1, e2, _) ->
+      (match inner e1, inner e2 with
+       | Some c1, Some c2 -> failwith "This shouldn't happen"
+       | None, None -> None
+       | c, None | None, c -> c)
+    | Const (CInt (c, _, _)) -> if Z.compare c Z.zero = 0 then None else Some (c |> cilint_to_int |> Rat.of_int)
+    | BinOp (Mult, _, _, _) -> None
+    | BinOp (Mod, _, _, _) -> None
+    | Lval (Var v, _) -> None
+    | _ -> failwith "found something else"
+  in
+  match e with
+  | BinOp (Le, e1, e2, _) ->
+    (match inner e1, inner e2 with
+     | Some c1, Some c2 -> failwith "This shouldn't happen"
+     | None, None -> Rat.zero
+     | Some c, None -> Rat.neg c
+     | None, Some c -> c)
+  | _ -> failwith "This shouldn't happen"
+
+let const_in_lincons1 (e: Lincons1.t) =
+  match Lincons1.get_cst e with
+  | Interval _ -> failwith "Lincons1 coeff is an interval, this shouldn't happen"
+  | Scalar s ->
+    match e.lincons0.typ with
+    | SUPEQ -> s |> SharedFunctions.int_of_scalar |> Option.get |> Z.to_int |> Rat.of_int (* don't negate here because cst is on the correct side *)
+    | _ -> failwith "wrong typ"
+
+let transposed_matrices_of_exp_list id (cs : exp list) =
+  let rec vars_from_exp acc = function
+    | BinOp (_, e1, e2, _) -> StringSet.union (vars_from_exp acc e1) (vars_from_exp acc e2)
+    | UnOp (_, e, _) -> vars_from_exp acc e
+    | Lval (Var v, _) ->
+      (match String.split_on_char '_' v.vname with
+       | "id"::_::"old"::_ -> acc (* TODO: maybe I'm forgetting too much here, could keep old_vars with the correct id *)
+       | _ -> StringSet.add v.vname acc)
+    | CastE _ -> failwith "Encountered cast"
+    | Question _ -> failwith "Encountered question"
+    | _ -> acc
+  in
+  let vars = cs |> List.fold_left vars_from_exp StringSet.empty |> StringSet.elements in
+  let old_vars = List.map (String.cat @@ "id_" ^ id ^ "_old_") vars in
+  (* TODO: could this result in invalid expressions where some terms are missing? *)
+  let atr = List.fold_left (fun m v -> cs |> List.map (coeff_in_exp v) |> SparseVec.of_list |> Matrix.append_row m) (Matrix.empty ()) old_vars in
+  let a'tr = List.fold_left (fun m v -> cs |> List.map (coeff_in_exp v) |> SparseVec.of_list |> Matrix.append_row m) (Matrix.empty ()) vars in
+  let b = cs |> List.map const_in_exp |> SparseVec.of_list in
+  atr, a'tr, b
+
+let transposed_matrices_of_lincons1set id (cs : Lincons1Set.t) =
+  let to_supeq_set e a =
+    match Lincons1.get_typ e with
+    | SUPEQ -> Lincons1Set.add e a
+    | EQ ->
+      let pos_e = Lincons1.make (Lincons1.get_linexpr1 e) SUPEQ in
+      let neg_e = Lincons1.make (Linexpr1.neg (Lincons1.get_linexpr1 e)) SUPEQ in
+      a |> Lincons1Set.add pos_e |> Lincons1Set.add neg_e
+    | _ -> failwith "Wrong typ in Lincons1Set"
+  in
+  let c = Lincons1Set.find_first (Fun.const true) cs in
+  let remove_old v =
+    match v |> Var.to_string |> String.split_on_char '_' with
+    | "id"::_::"old"::_ -> false (* TODO: maybe I'm forgetting too much here, could keep old_vars with the correct id *)
+    | _ -> true
+  in
+  let vars, _ = Environment.vars c.env in
+  let vars = vars |> Array.to_list |> List.filter remove_old in
+  let cs = Lincons1Set.fold to_supeq_set cs Lincons1Set.empty in
+  let atr = List.fold_left
+      (fun m v -> cs |> Lincons1Set.elements |>
+        List.map (coeff_in_lincons1 (Printf.sprintf "id_%s_old_%s" id (Var.to_string v))) |> SparseVec.of_list |> Matrix.append_row m) (Matrix.empty ()) vars in
+  let a'tr = List.fold_left (fun m v -> cs |> Lincons1Set.elements |> List.map (coeff_in_lincons1 (Var.to_string v)) |> SparseVec.of_list |> Matrix.append_row m) (Matrix.empty ()) vars in
+  let b = cs |> Lincons1Set.elements |> List.map const_in_lincons1 |> SparseVec.of_list in
+  atr, a'tr, b
+
+let string_of_my_invariant (constraints : MyInvariant.t) =
+  match constraints with
+  | `Top -> "Top"
+  | `Bot -> "Bot"
+  | `Lifted cs -> cs |> Lincons1Set.elements |> List.map Lincons1.show |> String.concat "; "
+
+let termination_provable a_transposed a'_transposed b =
+  let num_constraints = Matrix.num_cols a_transposed in
+  let zero, one, m_one = Sim.Core.R2.zero, Sim.Core.R2.of_r Rat.one, Sim.Core.R2.of_r Rat.m_one in
+  let ass_l1_a'tr_eq_zero sim =
+    let rec aux i sim =
+      if i >= Matrix.num_rows a'_transposed then sim else
+        let l1_ri = Matrix.get_row a'_transposed i
+          |> SparseVec.to_sparse_list
+          |> List.map (fun (idx, v) -> "x" ^ string_of_int idx, v)
+        in
+        if M.tracing then
+          M.trace "termination" "l1_r%i = %s" i
+            (l1_ri |> List.map (fun (var, value) -> (Printf.sprintf "(%s * %s)" (Rat.to_string value) var)) |> String.concat " + ");
+
+        let sim = fst @@
+          match l1_ri with
+          | [] -> sim, false
+          | [(var, _)] -> Sim.Assert.var sim var
+                            ~min:{Sim.Core.bvalue = zero; explanation = Ex.singleton (var ^ ">=0")}
+                            ~max:{Sim.Core.bvalue = zero; explanation = Ex.singleton (var ^ "<=0")}
+          | _ ->
+            let l1_ri = l1_ri |> Sim.Core.P.from_list in
+            Sim.Assert.poly sim l1_ri ("l1_r" ^ string_of_int i)
+              ~min:{Sim.Core.bvalue = zero; explanation = Ex.singleton ("l1_r" ^ string_of_int i ^ ">=0")}
+              ~max:{Sim.Core.bvalue = zero; explanation = Ex.singleton ("l1_r" ^ string_of_int i ^ "<=0")}
+        in aux (i + 1) sim
+    in aux 0 sim
+  in
+  let ass_l1_minus_l2_atr_eq_zero sim =
+    let rec aux i sim =
+      if i >= Matrix.num_rows a_transposed then sim else
+        let l1_m_l2_ri = Matrix.get_row a_transposed i
+          |> SparseVec.to_sparse_list
+          (* Example: (2, 0, -3) -> x0 * 2 + y0 * (-2) + x2 * (-3) + y2 * (-(-3))
+             map doesn't work here because we double the number of list elements *)
+          |> List.fold_left (fun l (idx, v) -> ("x" ^ string_of_int idx, v) :: ("y" ^ string_of_int idx, Rat.mul Rat.m_one v) :: l) []
+        in
+        if M.tracing then
+          M.trace "termination" "l1_m_l2_r%i = %s" i
+            (l1_m_l2_ri |> List.map (fun (var, value) -> (Printf.sprintf "(%s * %s)" (Rat.to_string value) var)) |> String.concat " + ");
+
+        let sim = fst @@
+          match l1_m_l2_ri with
+          | [] -> sim, false
+          | _ ->
+            let l1_m_l2_ri = Sim.Core.P.from_list l1_m_l2_ri in
+            Sim.Assert.poly sim l1_m_l2_ri ("l1_m_l2_r" ^ string_of_int i)
+              ~min:{Sim.Core.bvalue = zero; explanation = Ex.singleton ("l1_m_l2_r" ^ string_of_int i ^ ">=0")}
+              ~max:{Sim.Core.bvalue = zero; explanation = Ex.singleton ("l1_m_l2_r" ^ string_of_int i ^ "<=0")}
+        in aux (i + 1) sim
+    in aux 0 sim
+  in    
+  let ass_l2_atr_plus_a'tr_eq_zero sim =
+    let m = Matrix.add a_transposed a'_transposed in
+    let rec aux i sim =
+      if i >= Matrix.num_rows m then sim else
+        let l2_ri = Matrix.get_row m i
+          |> SparseVec.to_sparse_list
+          |> List.map (fun (idx, v) -> "y" ^ string_of_int idx, v)
+        in
+        if M.tracing then
+          M.trace "termination" "l2_r%i = %s" i
+            (l2_ri |> List.map (fun (var, value) -> (Printf.sprintf "(%s * %s)" (Rat.to_string value) var)) |> String.concat " + ");
+
+        let sim = fst @@
+          match l2_ri with
+          | [] -> sim, false
+          | [(var, _)] -> Sim.Assert.var sim var
+                            ~min:{Sim.Core.bvalue = zero; explanation = Ex.singleton (var ^ ">=0")}
+                            ~max:{Sim.Core.bvalue = zero; explanation = Ex.singleton (var ^ "<=0")}
+          | _ -> let l2_ri = l2_ri |> Sim.Core.P.from_list in
+            Sim.Assert.poly sim l2_ri ("l2_r" ^ string_of_int i)
+              ~min:{Sim.Core.bvalue = zero; explanation = Ex.singleton ("l2_r" ^ string_of_int i ^ ">=0")}
+              ~max:{Sim.Core.bvalue = zero; explanation = Ex.singleton ("l2_r" ^ string_of_int i ^ "<=0")}
+        in aux (i + 1) sim
+    in aux 0 sim
+  in
+  let ass_l2_b_lt_zero sim =
+    let l2_b = b
+      |> SparseVec.to_sparse_list
+      |> List.map (fun (i, v) -> "y" ^ string_of_int i, v)
+    in
+    if M.tracing then
+      M.trace "termination" "l2_b = %s"
+        (l2_b |> List.map (fun (var, value) -> (Printf.sprintf "(%s * %s)" (Rat.to_string value) var)) |> String.concat " + ");
+
+    fst @@
+    match l2_b with
+    | [] -> sim, false
+    | [(var, value)] when Rat.compare value Rat.zero > 0 -> Sim.Assert.var sim var
+                                                              ~max:{Sim.Core.bvalue = m_one; explanation = Ex.singleton (var ^ "<0")} (* creates a contradiction *)
+    | [(var, value)] when Rat.compare value Rat.zero < 0 -> Sim.Assert.var sim var
+                                                              ~min:{Sim.Core.bvalue = one; explanation = Ex.singleton (var ^ ">0")}
+    | [(var, _)] -> failwith "This shouldn't happen"
+    | _ -> let l2_b = Sim.Core.P.from_list l2_b in
+      Sim.Assert.poly sim l2_b "l2_b"
+        ~max:{Sim.Core.bvalue = m_one; explanation = Ex.singleton "l2_b<0"}
+  in
+  let ass_li_ge_zero sim =
+    let f sim i =
+      let sim', _ =
+        Sim.Assert.var sim ("x" ^ string_of_int i)
+          ~min:{Sim.Core.bvalue = zero; explanation = Ex.singleton ("x" ^ string_of_int i ^ ">=0")}
+      in
+      fst @@ Sim.Assert.var sim' ("y" ^ string_of_int i)
+        ~min:{Sim.Core.bvalue = zero; explanation = Ex.singleton ("y" ^ string_of_int i ^ ">=0")}
+    in
+    List.fold_left f sim (List.init num_constraints Fun.id)
+  in
+  let sim = Sim.Core.empty ~is_int:true ~check_invs:true
+    |> ass_l1_a'tr_eq_zero |> ass_l1_minus_l2_atr_eq_zero |> ass_l2_atr_plus_a'tr_eq_zero |> ass_l2_b_lt_zero |> ass_li_ge_zero
+    |> Sim.Solve.solve in
+  match sim.status with
+  | UNSAT _ -> false
+  | SAT -> true
+  | UNK -> failwith "Simplex returned UNK, this shouldn't happen"
+
 (** Checks whether a variable can be bounded. *)
 let ask_bound man varinfo =
   let open IntDomain.IntDomTuple in
@@ -62,7 +380,23 @@ struct
                   M.success ~category:Termination ~loc "Loop terminates: bounded by %a iteration(s)" IntDomain.IntDomTuple.pretty bound;
             end
           | None ->
-            failwith "Encountered a call to __goblint_bounded with an unknown loop counter variable."
+            (*failwith "Encountered a call to __goblint_bounded with an unknown loop counter variable."*)
+            let loop_id = loop_counter.vname |> String.split_on_char '_' |> (function _::id::_ -> id | _ -> "-1")
+            in
+            (*let atr, a'tr, b = man.ask (Queries.Invariant Invariant.default_context) |> exp_list_of_constraints |> transposed_matrices_of_exp_list loop_id in*)
+
+            let my_inv = man.ask (Queries.MyInvariant MyInvariant.default_context) in
+            let lincons1set =
+              match my_inv with
+              | `Lifted cs -> cs
+              | `Top | `Bot -> Lincons1Set.empty
+            in
+            let atr, a'tr, b = transposed_matrices_of_lincons1set loop_id lincons1set in
+
+            let term_provable = termination_provable atr a'tr b in
+            if term_provable then ((*if GobConfig.get_bool "dbg.termination-bounds" then*) M.success ~category:Termination "Loop terminates")
+            else (M.warn ~category:Termination "The program might not terminate!")
+
         end
       | "__goblint_bounded", _ ->
         failwith "__goblint_bounded call unexpected arguments"
diff --git a/src/cdomain/value/domains/invariant.ml b/src/cdomain/value/domains/invariant.ml
index 03cd57634b..de66b5127d 100644
--- a/src/cdomain/value/domains/invariant.ml
+++ b/src/cdomain/value/domains/invariant.ml
@@ -62,7 +62,7 @@ struct
 end
 
 
-(** Lift {!ExpLat} such that join/meet folds don't introduce excessive [|| 0|] or [&& 1] expressions. *)
+(** Lift {!ExpLat} such that join/meet folds don't introduce excessive [|| 0] or [&& 1] expressions. *)
 
 module N =
 struct
diff --git a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml
index 3cf017f163..6b3ed09f59 100644
--- a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml
+++ b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml
@@ -11,6 +11,7 @@ let timing_wrap = Vector.timing_wrap
 module type SparseMatrix =
 sig
   include Matrix
+  val add: t -> t -> t
   val get_col_upper_triangular: t -> int -> vec
 
   val swap_rows: t -> int -> int -> t
@@ -508,4 +509,6 @@ module ListMatrix: SparseMatrixFunctor =
       if M.tracing then M.tracel "linear_disjunct" "linear_disjunct between \n%s and \n%s =>\n%s" (show m1)  (show m2) (show res);
       res
 
+  let add = List.map2 V.add
+
   end
diff --git a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml
index 71d4a27016..16025efe4c 100644
--- a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml
+++ b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml
@@ -8,6 +8,7 @@ open Batteries
 module type SparseVector =
 sig
   include Vector
+  val add: t -> t -> t
   val push_first: t -> int -> num -> t
 
   val is_zero_vec: t -> bool
@@ -367,4 +368,18 @@ module SparseVector: SparseVectorFunctor =
     let rev v =
       let entries = List.rev_map (fun (idx, value) -> (v.len - 1 - idx, value)) v.entries in
       {entries; len = v.len}
+
+    let add a b =
+      if a.len <> b.len then raise (Invalid_argument "Unequal lengths") else
+        let rec aux a b =
+          match a, b with
+          | [], b -> b
+          | a, [] -> a
+          | (ix, vx)::xs, (iy, vy)::ys when ix = iy ->
+            let sum = A.add vx vy in
+            if sum = A.zero then aux xs ys
+            else (ix, sum) :: aux xs ys
+          | (ix, vx)::xs, (iy, _)::_ when ix < iy -> (ix, vx) :: aux xs b
+          | _, y::ys -> y :: aux a ys
+        in {entries = aux a.entries b.entries; len = a.len}
   end
diff --git a/src/cdomains/apron/affineEqualityDenseDomain.apron.ml b/src/cdomains/apron/affineEqualityDenseDomain.apron.ml
index 1db52f15a2..c49c9ec726 100644
--- a/src/cdomains/apron/affineEqualityDenseDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDenseDomain.apron.ml
@@ -596,6 +596,8 @@ struct
     in
     BatOption.map_default invariant [] t.d
 
+  let invariant_set _ = failwith "not needed here"
+
   let cil_exp_of_lincons1 = Convert.cil_exp_of_lincons1
 
   let env t = t.env
diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 06e131bbec..4f4c219f8d 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -547,6 +547,8 @@ struct
     in
     BatOption.map_default invariant [] t.d
 
+  let invariant_set _ = failwith "not needed here"
+
   let cil_exp_of_lincons1 = Convert.cil_exp_of_lincons1
 
   let env t = t.env
diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index 2273ec5306..2c81046259 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -555,7 +555,7 @@ struct
   let to_lincons_set d =
     Lincons1Set.of_earray (A.to_lincons_array Man.mgr d)
 
-  let invariant d =
+  let invariant_set d =
     (* Would like to minimize to get rid of multi-var constraints directly derived from one-var constraints,
        but not implemented in Apron at all: https://github.com/antoinemine/apron/issues/44 *)
     (* let d = A.copy Man.mgr d in
@@ -572,9 +572,15 @@ struct
       lcd
 
   let invariant d =
-    invariant d
+    let res =
+    invariant_set d
     |> (if Oct.manager_is_oct Man.mgr then Lincons1Set.simplify else Fun.id)
     |> Lincons1Set.elements (* TODO: remove list conversion? *)
+    in
+    if M.tracing then
+      (M.trace "termination" "RD.invariant: (%s)" (res |> List.map Lincons1.show |> String.concat ", "));
+    res
+
 end
 
 (** With heterogeneous environments. *)
diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
index e5c89d0e80..1ebe6a725c 100644
--- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
+++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
@@ -813,6 +813,8 @@ struct
     in
     BatOption.get t.d |> fun (_,map) -> EConj.IntMap.fold (fun lhs rhs list -> get_const list lhs rhs) map []
 
+  let invariant_set _ = failwith "not needed here"
+
   let cil_exp_of_lincons1 = Convert.cil_exp_of_lincons1
 
   let env t = t.env
diff --git a/src/cdomains/apron/myInvariant.ml b/src/cdomains/apron/myInvariant.ml
new file mode 100644
index 0000000000..61dc724733
--- /dev/null
+++ b/src/cdomains/apron/myInvariant.ml
@@ -0,0 +1,55 @@
+open GoblintCil
+open GobApron
+
+(** Symbolic (and fully syntactic) expression "lattice". *)
+module MyExp =
+struct
+  include Lincons1Set
+
+  let hash _ = failwith "TODO"
+  let show _ = failwith "TODO"
+  let pretty _ = failwith "TODO"
+  let printXml _ = failwith "TODO"
+  let name _ = failwith "TODO"
+  let to_yojson _ = failwith "TODO"
+  let tag _ = failwith "TODO"
+  let arbitrary _ = failwith "TODO"
+  let relift _ = failwith "TODO"
+  let leq _ _ = failwith "ExpLat: leq" (* cannot say for sure, requires general entailment check *)
+  let pretty_diff () _ = failwith "ExpLat: pretty_diff" (* irrelevant, no leq *)
+  let join x y = failwith "TODO"
+  let meet x y = failwith "TODO"
+  let widen x y = y
+  let narrow = meet
+  let to_lincons1_set t : Lincons1Set.t = t
+end
+
+
+(** Lift {!ExpLat} such that join/meet folds don't introduce excessive [|| 0] or [&& 1] expressions. *)
+
+module N =
+struct
+  include Printable.DefaultConf
+  let bot_name = "false"
+  let top_name = "true"
+end
+
+include Lattice.LiftConf (N) (MyExp)
+
+let none = top ()
+let of_lincons1_set = lift
+
+let ( && ) = meet
+let ( || ) = join
+
+let to_lincons1_set t : Lincons1Set.t = MyExp.to_lincons1_set t
+
+type context = {
+  path: int option;
+  lvals: Lval.Set.t;
+}
+
+let default_context = {
+  path = None;
+  lvals = Lval.Set.top ();
+}
diff --git a/src/cdomains/apron/relationDomain.apron.ml b/src/cdomains/apron/relationDomain.apron.ml
index 5d266cf474..bd88791ab6 100644
--- a/src/cdomains/apron/relationDomain.apron.ml
+++ b/src/cdomains/apron/relationDomain.apron.ml
@@ -137,6 +137,7 @@ sig
   include S2
   val cil_exp_of_lincons1: Lincons1.t -> exp option
   val invariant: t -> Lincons1.t list
+  val invariant_set: t -> Lincons1Set.t
 end
 
 type ('a, 'b) relcomponents_t = {
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 53c8db8099..cbe0d84452 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -301,8 +301,9 @@ struct
   (** Returned boolean indicates whether returned expression should be negated. *)
   let cil_exp_of_linexpr1_term ~scalewith (c: Coeff.t) v =
     match V.to_cil_varinfo v with
-    | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[]))   ->
-      let var = Cilfacade.mkCast ~kind:Explicit ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
+    | Some vinfo (*when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[]))  *) ->
+      (*let var = Cilfacade.mkCast ~kind:Explicit ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in*)
+      let var = (Lval(Var vinfo,NoOffset)) in
       let i = int_of_coeff_warn ~scalewith c in
       if Z.equal i Z.one then
         false, var
@@ -316,9 +317,9 @@ struct
     | None ->
       M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %a" Var.pretty v;
       raise Unsupported_Linexpr1
-    | _ ->
+    (*| _ ->
       M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %a" Var.pretty v;
-      raise Unsupported_Linexpr1
+      raise Unsupported_Linexpr1*)
 
   (** Returned booleans indicates whether returned expressions should be negated. *)
   let cil_exp_of_linexpr1 ~scalewith (linexpr1:Linexpr1.t) =
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 6b85a2729c..23bf82af32 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -74,6 +74,11 @@ type invariant_context = Invariant.context = {
   lvals: Lval.Set.t;
 }
 [@@deriving ord, hash]
+type my_invariant_context = MyInvariant.context = {
+  path: int option;
+  lvals: Lval.Set.t;
+}
+[@@deriving ord, hash]
 
 module YS = SetDomain.ToppedSet (YamlWitnessType.Entry) (struct let topname = "Top" end)
 
@@ -147,6 +152,7 @@ type _ t =
   | GhostVarAvailable: WitnessGhostVar.t -> MayBool.t t
   | InvariantGlobalNodes: NS.t t (** Nodes where YAML witness flow-insensitive invariants should be emitted as location invariants (if [witness.invariant.flow_insensitive-as] is configured to do so). *) (* [Spec.V.t] argument (as [Obj.t]) could be added, if this should be different for different flow-insensitive invariants. *)
   | DescendantThreads: ThreadIdDomain.Thread.t -> ConcDomain.ThreadSet.t t
+  | MyInvariant: my_invariant_context -> MyInvariant.t t
 
 type 'a result = 'a
 
@@ -223,6 +229,7 @@ struct
     | GhostVarAvailable _ -> (module MayBool)
     | InvariantGlobalNodes -> (module NS)
     | DescendantThreads _ -> (module ConcDomain.ThreadSet)
+    | MyInvariant _ -> (module MyInvariant)
 
   (** Get bottom result for query. *)
   let bot (type a) (q: a t): a result =
@@ -298,6 +305,7 @@ struct
     | GhostVarAvailable _ -> MayBool.top ()
     | InvariantGlobalNodes -> NS.top ()
     | DescendantThreads _ -> ConcDomain.ThreadSet.top ()
+    | MyInvariant _ -> MyInvariant.top ()
 end
 
 (* The type any_query can't be directly defined in Any as t,
@@ -370,6 +378,7 @@ struct
     | Any (GhostVarAvailable _) -> 62
     | Any InvariantGlobalNodes -> 63
     | Any (DescendantThreads _) -> 64
+    | Any (MyInvariant _) -> 65
 
   let rec compare a b =
     let r = Stdlib.compare (order a) (order b) in
@@ -430,6 +439,7 @@ struct
       | Any (GasExhausted f1), Any (GasExhausted f2) -> CilType.Fundec.compare f1 f2
       | Any (GhostVarAvailable v1), Any (GhostVarAvailable v2) -> WitnessGhostVar.compare v1 v2
       | Any (DescendantThreads t1), Any (DescendantThreads t2) -> ThreadIdDomain.Thread.compare t1 t2
+      | Any (MyInvariant i1), Any (MyInvariant i2) -> compare_my_invariant_context i1 i2
       (* only argumentless queries should remain *)
       | _, _ -> Stdlib.compare (order a) (order b)
 
@@ -478,6 +488,7 @@ struct
     | Any (GasExhausted f) -> CilType.Fundec.hash f
     | Any (GhostVarAvailable v) -> WitnessGhostVar.hash v
     | Any (DescendantThreads t) -> ThreadIdDomain.Thread.hash t
+    | Any (MyInvariant i) -> hash_my_invariant_context i
     (* IterSysVars:                                                                    *)
     (*   - argument is a function and functions cannot be compared in any meaningful way. *)
     (*   - doesn't matter because IterSysVars is always queried from outside of the analysis, so MCP's query caching is not done for it. *)
@@ -547,6 +558,7 @@ struct
     | Any (GhostVarAvailable v) -> Pretty.dprintf "GhostVarAvailable %a" WitnessGhostVar.pretty v
     | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes"
     | Any (DescendantThreads t) -> Pretty.dprintf "DescendantThreads %a" ThreadIdDomain.Thread.pretty t
+    | Any (MyInvariant i) -> Pretty.dprintf "MyInvariant _"
 end
 
 let to_value_domain_ask (ask: ask) =
diff --git a/src/dune b/src/dune
index 2b5f369e30..385f132c21 100644
--- a/src/dune
+++ b/src/dune
@@ -7,7 +7,7 @@
   (name goblint_lib)
   (public_name goblint.lib)
   (modules :standard \ goblint privPrecCompare apronPrecCompare messagesCompare)
-  (libraries goblint.sites goblint.build-info goblint-cil goblint-cil.pta goblint-cil.syntacticsearch batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_constraint goblint_solver goblint_library goblint_cdomain_value goblint_incremental goblint_tracing goblint_logs domain_shims
+  (libraries goblint.sites goblint.build-info goblint-cil goblint-cil.pta goblint-cil.syntacticsearch batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_constraint goblint_solver goblint_library goblint_cdomain_value goblint_incremental goblint_tracing goblint_logs domain_shims ocplib-simplex
     ; Conditionally compile based on whether apron optional dependency is installed or not.
     ; Alternative dependencies seem like the only way to optionally depend on optional dependencies.
     ; See: https://dune.readthedocs.io/en/stable/reference/library-dependencies.html#alternative-dependencies
@@ -92,7 +92,7 @@
   (public_names goblint)
   (modes byte native) ; https://dune.readthedocs.io/en/stable/dune-files.html#linking-modes
   (modules goblint)
-  (libraries goblint.lib goblint_std)
+  (libraries goblint.lib goblint_std ocplib-simplex)
   (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson))
   (flags :standard -linkall -open Goblint_std)
   (instrumentation (backend bisect_ppx))
diff --git a/src/util/terminationPreprocessing.ml b/src/util/terminationPreprocessing.ml
index 95fae95d26..eb12e124d4 100644
--- a/src/util/terminationPreprocessing.ml
+++ b/src/util/terminationPreprocessing.ml
@@ -2,6 +2,7 @@ open GoblintCil
 (* module Z = Big_int_Z *)
 
 module VarToStmt = Map.Make(CilType.Varinfo) (* maps varinfos (= loop counter variable) to the statement of the corresponding loop*)
+module VarSet = Set.Make(CilType.Varinfo)
 
 let counter_ikind = IULongLong
 let counter_typ = TInt (counter_ikind, [])
@@ -12,6 +13,16 @@ let min_int_exp =
   else
     Const(CInt(Z.zero, counter_ikind, None))
 
+let string_of_loop_info loop_info =
+  String.concat "; " (List.map (fun s -> match s.skind with
+      | Instr is -> Printf.sprintf "Instrs(%s)" (String.concat "; " (List.map
+                                                                       (fun i -> match i with | Set ((Var v, _), _, loc, _) -> Printf.sprintf "%i: %s" loc.line v.vname | Call _ -> "Call" | _ -> "Some other instr") is))
+      | Break _ -> "Break"
+      | If _ -> "If"
+      | _ -> "Something else") loop_info)
+
+let rec exisis_nested_loop = List.exists (fun s -> match s.skind with Loop _ -> true | _ -> false)
+
 class loopCounterVisitor lc (fd : fundec) = object(self)
   inherit nopCilVisitor
 
@@ -46,18 +57,73 @@ class loopCounterVisitor lc (fd : fundec) = object(self)
 
     let action s = match s.skind with
       | Loop (b, loc, eloc, _, _) ->
-        let vname = "term" ^ string_of_int loc.line ^ "_" ^ string_of_int loc.column ^ "_id" ^ (string_of_int !vcounter) in
-        incr vcounter;
-        let v = Cil.makeLocalVar fd vname counter_typ in (*Not tested for incremental mode*)
-        let lval = Lval (Var v, NoOffset) in
-        let init_stmt = mkStmtOneInstr @@ Set (var v, min_int_exp, loc, eloc) in
-        let inc_stmt = mkStmtOneInstr @@ Set (var v, increment_expression lval, loc, eloc) in
-        let exit_stmt = mkStmtOneInstr @@ Call (None, f_bounded, [lval], loc, locUnknown) in
-        b.bstmts <- exit_stmt :: inc_stmt :: b.bstmts;
-        lc := VarToStmt.add (v: varinfo) (s: stmt) !lc;
-        let nb = mkBlock [init_stmt; mkStmt s.skind] in
-        s.skind <- Block nb;
+        (*let vname = "term" ^ string_of_int loc.line ^ "_" ^ string_of_int loc.column ^ "_id" ^ (string_of_int !vcounter) in
+          incr vcounter;
+          let v = Cil.makeLocalVar fd vname counter_typ in (*Not tested for incremental mode*)
+          let lval = Lval (Var v, NoOffset) in
+          let init_stmt = mkStmtOneInstr @@ Set (var v, min_int_exp, loc, eloc) in
+          let inc_stmt = mkStmtOneInstr @@ Set (var v, increment_expression lval, loc, eloc) in
+          let exit_stmt = mkStmtOneInstr @@ Call (None, f_bounded, [lval], loc, locUnknown) in
+          (*Printf.printf "Before additions\n%s\n\n" (string_of_loop_info b.bstmts);*)
+          b.bstmts <- exit_stmt :: inc_stmt :: b.bstmts;
+          lc := VarToStmt.add (v: varinfo) (s: stmt) !lc;
+          let nb = mkBlock [init_stmt; mkStmt s.skind] in
+          s.skind <- Block nb;*)
+
+        incr vcounter; (* TODO: synchronize with existing termination analysis *)
+
+        let rec vars_from_exp = function
+          | BinOp (_, e1, e2, _) -> VarSet.union (vars_from_exp e1) (vars_from_exp e2)
+          | UnOp (_, e, _) -> vars_from_exp e
+          | Lval (Var v, _) -> VarSet.singleton v
+          | CastE (_, _, e) -> vars_from_exp e (* TODO: special handling needed? *)
+          | Question _ -> failwith "Encountered question"
+          | _ -> VarSet.empty
+        in
+        let rec get_vars = function
+          | [] -> VarSet.empty
+          | s::ss -> (match s.skind with
+              | Instr instrs ->
+                let rec get_vars_helper = function
+                  | [] -> get_vars ss
+                  | i::is -> (match i with
+                      | Set ((Var v, NoOffset), e, _, _) -> (match v.vtype with
+                          | TInt (_, _) -> VarSet.union (VarSet.add v (vars_from_exp e)) (get_vars_helper is)
+                          | _ -> get_vars_helper is)
+                      | _ -> get_vars_helper is) in
+                get_vars_helper instrs
+              | If (e, b1, b2, _, _) -> vars_from_exp e |> VarSet.union (get_vars b1.bstmts) |> VarSet.union (get_vars b2.bstmts) |> VarSet.union (get_vars ss)
+              | Break _ -> (*Printf.printf "\nfound a break\n";*) get_vars ss
+              | _ -> get_vars ss)
+        in
+        let vars = get_vars b.bstmts |> VarSet.elements in
+
+        if vars <> [] then (
+          match b.bstmts with
+          | [] -> ()
+          | s1 :: ss ->
+            match s1.skind with
+             | If (_, _, _, loc, eloc) ->
+               let lval v = Lval (Var v, NoOffset) in
+               let init_old_var v =
+                 let old_vname = "id_" ^ (string_of_int !vcounter) ^ "_old_" ^ v.vname in
+                 let old_v = Cil.makeLocalVar fd old_vname v.vtype in
+                 Set (var old_v, lval v, loc, eloc)
+               in
+               let init_old_vars = List.map init_old_var vars in
+               let first_old_var =
+                 match List.hd init_old_vars with
+                 | Set ((Var first_old_var, NoOffset), _, _, _) -> first_old_var
+                 | _ -> failwith "impossible"
+               in
+               b.bstmts <- s1 ::
+                           mkStmt (Instr init_old_vars) ::
+                           ss @
+                           [mkStmtOneInstr (Call (None, f_bounded, [lval first_old_var], loc, eloc))]; (* TODO: replace f_bounded by something appropriate; replace loc by the correct location *)
+             | _ -> (*Printf.printf "Some other structure\n"*) ()
+        );
         s
+
       | Goto (sref, l) ->
         let goto_jmp_stmt = sref.contents in
         let loc_stmt = Cilfacade.get_stmtLoc goto_jmp_stmt in
diff --git a/tests/regression/78-termination/52-synthesis-ranking.c b/tests/regression/78-termination/52-synthesis-ranking.c
new file mode 100644
index 0000000000..21bd8bade2
--- /dev/null
+++ b/tests/regression/78-termination/52-synthesis-ranking.c
@@ -0,0 +1,16 @@
+// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra
+
+// from: https://www.cs.cmu.edu/~hzarnani/fm-rg/cmuonly/podelski04complete.pdf, Example 1
+// Ranking function: i - j
+
+#include <stdlib.h>
+int main() {
+    int i, j, nat, pos;
+    __goblint_assume(nat >= 0);
+    __goblint_assume(pos >= 1);
+
+    while (i - j >= 1) {
+        j = j + pos;
+        i = i - nat;
+    }
+}
\ No newline at end of file
diff --git a/tests/regression/78-termination/53-synthesis-ranking-2.c b/tests/regression/78-termination/53-synthesis-ranking-2.c
new file mode 100644
index 0000000000..4d82f2d043
--- /dev/null
+++ b/tests/regression/78-termination/53-synthesis-ranking-2.c
@@ -0,0 +1,16 @@
+// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra
+
+// from: https://www.cs.unipr.it/~zaffanella/Papers/PDF/Q498.pdf, Example 4.6
+// Ranking function: x1
+
+#include <stdlib.h>
+
+int main() {
+    int x1;
+    int x2 = 0;
+
+    while (x1 >= 2) {
+        x1 = x1 / 2;
+        x2++;
+    }
+}
diff --git a/tests/regression/78-termination/54-synthesis-impossible.c b/tests/regression/78-termination/54-synthesis-impossible.c
new file mode 100644
index 0000000000..8485168150
--- /dev/null
+++ b/tests/regression/78-termination/54-synthesis-impossible.c
@@ -0,0 +1,13 @@
+// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra
+
+// from: https://www.cs.cmu.edu/~hzarnani/fm-rg/cmuonly/podelski04complete.pdf, Example 2
+// There is NO linear ranking function here (x doesn't decrease monotonously, e.g. (5, 0, 10, -10))
+
+#include <stdlib.h>
+int main() {
+    int x;
+
+    while (x >= 0) {
+        x = -2 * x + 10;
+    }
+}
diff --git a/tests/regression/78-termination/55-synthesis-advantage.c b/tests/regression/78-termination/55-synthesis-advantage.c
new file mode 100644
index 0000000000..91fbdc00f1
--- /dev/null
+++ b/tests/regression/78-termination/55-synthesis-advantage.c
@@ -0,0 +1,18 @@
+// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra
+
+// x is strictly monotonously decreasing, but the classical termination analysis doesn't work
+
+#include <stdlib.h>
+
+int main() {
+    int x;
+
+    while (x >= 2) {
+        x = x == 42 ? x - 1 : x / 2;
+        /*if (x == 42) {
+            x--;
+        } else {
+            x = x / 2;
+        }*/
+    }
+}
diff --git a/tests/regression/78-termination/56-synthesis-advantage-2.c b/tests/regression/78-termination/56-synthesis-advantage-2.c
new file mode 100644
index 0000000000..86c37240c1
--- /dev/null
+++ b/tests/regression/78-termination/56-synthesis-advantage-2.c
@@ -0,0 +1,19 @@
+// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra
+
+// from: https://dl.acm.org/doi/pdf/10.1145/1941487.1941509, Figure 1
+// Linear ranking function, e.g.: 2x + y
+
+#include <stdlib.h>
+
+int main() {
+    int x, y;
+
+    while (x > 0 && y > 0) {
+        if (rand() == 0) {
+            x = x - 1;
+            y = y + 1;
+        } else {
+            y = y - 1;
+        }
+    }
+}
diff --git a/tests/regression/78-termination/57-synthesis-advantage-3.c b/tests/regression/78-termination/57-synthesis-advantage-3.c
new file mode 100644
index 0000000000..11726d19b3
--- /dev/null
+++ b/tests/regression/78-termination/57-synthesis-advantage-3.c
@@ -0,0 +1,19 @@
+// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra
+
+// from: https://dl.acm.org/doi/pdf/10.1145/1941487.1941509, Figure 2
+// Linear ranking function exists only if numbers are bounded (e.g.: 2^32x + y), otherwise lexicographic needed
+
+#include <stdlib.h>
+
+int main() {
+    int x, y;
+
+    while (x > 0 && y > 0) {
+        if (rand() == 0) {
+            x = x - 1;
+            y = rand();
+        } else {
+            y = y - 1;
+        }
+    }
+}