diff --git a/src/analyses/phaseGhost.ml b/src/analyses/phaseGhost.ml
index e04ba769a4..2555b82572 100644
--- a/src/analyses/phaseGhost.ml
+++ b/src/analyses/phaseGhost.ml
@@ -1,4 +1,5 @@
-(** Analysis for checking whether ghost globals are only accessed by one unique thread ([phaseGhost]). *)
+(** Analysis for checking whether ghost globals are only accessed by one unique thread
+    and monotonically increased to known bounds ([phaseGhost]). *)
 
 open Analyses
 open GoblintCil
@@ -12,10 +13,10 @@ struct
   let name () = "ghost-constant"
 end
 
-module IncByOne =
+module MonotoneBounded =
 struct
   include BoolDomain.MustBool
-  let name () = "increment-by-one"
+  let name () = "monotone-bounded"
 end
 
 module Spec =
@@ -33,11 +34,11 @@ struct
   module V = VarinfoV
   module G =
   struct
-    include Lattice.Prod (TIDs) (IncByOne)
+    include Lattice.Prod (TIDs) (MonotoneBounded)
     let tids = fst
-    let inc_by_one = snd
-    let create_tids tids = (tids, IncByOne.bot ())
-    let create_inc_by_one inc_by_one = (TIDs.bot (), inc_by_one)
+    let monotone_bounded = snd
+    let create_tids tids = (tids, MonotoneBounded.bot ())
+    let create_monotone_bounded monotone_bounded = (TIDs.bot (), monotone_bounded)
   end
 
   let initial_ghost_values () =
@@ -66,28 +67,6 @@ struct
     | `Lifted tid when TID.is_unique tid -> TIDs.singleton tid
     | _ -> TIDs.top ()
 
-  let increment_constant lval rval =
-    let is_same_lval e =
-      match Cil.stripCasts e with
-      | Lval lval' -> CilType.Lval.equal lval lval'
-      | _ -> false
-    in
-    let is_one_constant e =
-      match Cil.getInteger (Cil.constFold true e) with
-      | Some k -> Z.equal k Z.one
-      | None -> false
-    in
-    match Cil.stripCasts rval with
-    | BinOp (PlusA, e1, e2, _) ->
-      if is_same_lval e1 then
-        is_one_constant e2
-      else if is_same_lval e2 then
-        is_one_constant e1
-      else
-        false
-    | _ ->
-      false
-
   (* This local constant folding intentionally disregards writes from other threads.
      It is only for the phaseGhost checker itself. *)
   (* This information must **not** be used to refine other analyses or returned by any query,
@@ -121,11 +100,10 @@ struct
     | _ ->
       None
 
-  let is_increment_by_one state lval rval =
-    increment_constant lval rval ||
+  let is_monotone_bounded_update state lval rval =
     match eval_const state (Lval lval), eval_const state rval with
     | Some old_value, Some new_value ->
-      Z.equal new_value (Z.succ old_value)
+      Z.lt old_value new_value
     | _ ->
       false
 
@@ -153,13 +131,13 @@ struct
     else
       match lval with
       | Var var, NoOffset when YamlWitness.VarSet.mem var !(YamlWitness.ghostVars) ->
-        let inc_by_one = is_increment_by_one man.local lval rval in
+        let monotone_bounded = is_monotone_bounded_update man.local lval rval in
         let local =
-          match inc_by_one, eval_const man.local rval with
+          match monotone_bounded, eval_const man.local rval with
           | true, Some z -> D.add var (`Lifted z) man.local
           | _ -> D.add var (Const.top ()) man.local
         in
-        man.sideg var (G.create_inc_by_one inc_by_one);
+        man.sideg var (G.create_monotone_bounded monotone_bounded);
         local
       | _ ->
         man.local
@@ -176,8 +154,8 @@ struct
         | _ ->
           false
       in
-      let (tids, inc_by_one) = man.global var in
-      inc_by_one && unique_owner tids
+      let (tids, monotone_bounded) = man.global var in
+      monotone_bounded && unique_owner tids
     | Queries.Owner var when YamlWitness.VarSet.mem var !(YamlWitness.ghostVars) ->
       let tidset = G.tids (man.global var) in
       begin match TIDs.elements tidset with
@@ -190,16 +168,16 @@ struct
       end
     | Queries.WarnGlobal g ->
       let g: V.t = Obj.obj g in
-      let (tidset, inc_by_one) = man.global g in
+      let (tidset, monotone_bounded) = man.global g in
       if TIDs.is_top tidset then
         (M.warn_noloc ~category:Witness "phaseGhost: global %a is accessed by a non-unique or unknown thread id" CilType.Varinfo.pretty g;)
       else
         (match TIDs.elements tidset with
          | [tid] when TID.is_unique tid ->
-           if inc_by_one then
-             M.info_noloc ~category:Witness "phaseGhost: global %a is only accessed by unique thread %a and is only ever increased by one" CilType.Varinfo.pretty g TID.pretty tid
+           if monotone_bounded then
+             M.info_noloc ~category:Witness "phaseGhost: global %a is only accessed by unique thread %a and is monotonically increased to known bounds" CilType.Varinfo.pretty g TID.pretty tid
            else
-             M.warn_noloc ~category:Witness "phaseGhost: global %a is only accessed by unique thread %a, but is not only ever increased by one" CilType.Varinfo.pretty g TID.pretty tid
+             M.warn_noloc ~category:Witness "phaseGhost: global %a is only accessed by unique thread %a, but is not monotonically increased to known bounds" CilType.Varinfo.pretty g TID.pretty tid
          | _ ->
            M.warn_noloc ~category:Witness "phaseGhost: global %a is accessed by multiple unique threads: %a" CilType.Varinfo.pretty g TIDs.pretty tidset)
     | _ ->
diff --git a/src/analyses/phaseGhostSplit.ml b/src/analyses/phaseGhostSplit.ml
index 6141b01c4d..89d75065d4 100644
--- a/src/analyses/phaseGhostSplit.ml
+++ b/src/analyses/phaseGhostSplit.ml
@@ -1,4 +1,4 @@
-(** Analysis for checking whether ghost globals are only accessed by one unique thread ([phaseGhostSplit]). *)
+(** Analysis for propagating phase changes of ghost globals accepted by [phaseGhost]. *)
 
 open Analyses
 open GoblintCil
@@ -57,12 +57,14 @@ struct
     let create_const_at_thread_end const = (const, PhaseChanges.bot ())
     let create_change phase mhp pinfo = (Const.bot (), (PhaseChanges.singleton phase (MHPs.singleton mhp, pinfo)))
 
-    let can_change_to (_, changes) target currmhp =
-      match PhaseChanges.find_opt (`Lifted target) changes with
-      | Some (accesses, pinfo) when MHPs.can_any_mhp currmhp accesses ->
-        Some pinfo
-      | _ ->
-        None
+    let possible_changes_after (_, changes) current currmhp =
+      PhaseChanges.fold (fun target (accesses, pinfo) acc ->
+          match target with
+          | `Lifted target when Z.lt current target && MHPs.can_any_mhp currmhp accesses ->
+            (target, pinfo) :: acc
+          | _ ->
+            acc
+        ) changes []
   end
 
   let initial_ghost_values () =
@@ -105,28 +107,6 @@ struct
     | `Lifted tid when TID.is_unique tid -> TIDs.singleton tid
     | _ -> TIDs.top ()
 
-  let increment_constant lval rval =
-    let is_same_lval e =
-      match Cil.stripCasts e with
-      | Lval lval' -> CilType.Lval.equal lval lval'
-      | _ -> false
-    in
-    let is_one_constant e =
-      match Cil.getInteger (Cil.constFold true e) with
-      | Some k -> Z.equal k Z.one
-      | None -> false
-    in
-    match Cil.stripCasts rval with
-    | BinOp (PlusA, e1, e2, _) ->
-      if is_same_lval e1 then
-        is_one_constant e2
-      else if is_same_lval e2 then
-        is_one_constant e1
-      else
-        false
-    | _ ->
-      false
-
   (* This local constant folding intentionally disregards writes from other threads.
      It is only for the phaseGhost checker itself. *)
   (* This information must **not** be used to refine other analyses,
@@ -160,14 +140,6 @@ struct
     | _ ->
       None
 
-  let is_increment_by_one state lval rval =
-    increment_constant lval rval ||
-    match eval_const state (Lval lval), eval_const state rval with
-    | Some old_value, Some new_value ->
-      Z.equal new_value (Z.succ old_value)
-    | _ ->
-      false
-
   let current_mhp man: MCPAccess.A.t =
     Obj.obj (man.ask (PartAccess Point))
 
@@ -181,17 +153,17 @@ struct
       man.local
     else
       let local = top_non_phase_ghosts man man.local in
-      let may_be_advanced_here m var =
+      let possible_advances_here m var =
         if man.ask Queries.MustBeAtomic then
           (* Shortcut, would also be caught below, but as it is common cheaper to check here *)
-          (if M.tracing then M.tracel "phaseGhost" "Is atomic -> not advancing phase"; None)
+          (if M.tracing then M.tracel "phaseGhost" "Is atomic -> not advancing phase"; [])
         else
           match man.ask (Queries.Owner var), man.ask Queries.CurrentThreadId, D.find var m  with
           | `Bot, _, _
           | _, `Bot, _ ->
-            None
-          | `Lifted owner, _ , `Lifted z ->
-            G.can_change_to (man.global var) (Z.succ z) (current_mhp man)
+            []
+          | `Lifted _owner, _ , `Lifted z ->
+            G.possible_changes_after (man.global var) z (current_mhp man)
           | _ ->
             failwith "assumption about ghost owner violated"
       in
@@ -199,24 +171,18 @@ struct
         | []  ->
           man.split m [Events.PropAuxiliaryPhaseInfo (Obj.repr pinfo)]
         | var :: vars ->
-          match may_be_advanced_here m var with
-          | Some curr_pinfo ->
-            (let v' = (match (D.find var m) with
-                 | `Lifted x -> Z.succ x
-                 | _ -> failwith "assumption")
-             in
-             let advanced = D.add var (`Lifted v') m in
-             let pinfo' = MCPPhaseInfo.meet pinfo curr_pinfo in
-             handle_vars (advanced, pinfo') (var::vars);
-             handle_vars (m, pinfo) vars)
-          | None ->
-            handle_vars (m, pinfo) vars
+          List.iter (fun (target, curr_pinfo) ->
+              let advanced = D.add var (`Lifted target) m in
+              let pinfo' = MCPPhaseInfo.meet pinfo curr_pinfo in
+              handle_vars (advanced, pinfo') (var::vars)
+            ) (possible_advances_here m var);
+          handle_vars (m, pinfo) vars
       in
       let traceEvolution () =
         YamlWitness.VarSet.iter (fun var ->
             let owner = man.ask (Queries.Owner var) in
             let phase_ghost = is_phase_ghost man var in
-            let may_advance = phase_ghost && Option.is_some (may_be_advanced_here local var) in
+            let may_advance = phase_ghost && possible_advances_here local var <> [] in
             M.tracel "phaseGhost" "Ghost %a is %sa phase ghost, has owner %a and may %s be advanced here" (* nosemgrep: trace-not-in-tracing *)
               CilType.Varinfo.pretty var
               (if phase_ghost then "" else "not ")
@@ -238,17 +204,17 @@ struct
       | Var var, NoOffset when YamlWitness.VarSet.mem var !(YamlWitness.ghostVars) && not (is_phase_ghost man var) ->
         D.add var (Const.top ()) local
       | Var var, NoOffset when is_phase_ghost man var ->
-        (match eval_const local (Lval lval) with
-         | Some z ->
-           (let v = Z.succ z in
-            let local_new = D.add var (`Lifted v) local in
+        (match eval_const local (Lval lval), eval_const local rval with
+         | Some old_value, Some new_value when Z.lt old_value new_value ->
+           (let local_new = D.add var (`Lifted new_value) local in
             let local_pinfo = current_pinfo man in
-            man.sideg var (G.create_change (`Lifted v) (current_mhp man) (local_pinfo));
+            man.sideg var (G.create_change (`Lifted new_value) (current_mhp man) (local_pinfo));
             (* TODO: Prolong until after atomic is over? *)
             if not (D.equal local local_new) then
               man.emit (Events.PhaseChange {old_phase = `Lifted local; new_phase = `Lifted local_new});
             local_new)
-         | None -> failwith "Failed to evaluate ghost to constant")
+         | _ ->
+           D.add var (Const.top ()) local)
       | _ ->
         local
 
diff --git a/tests/regression/19-ghost-witness/02-empire-detect.t b/tests/regression/19-ghost-witness/02-empire-detect.t
index 778956e187..572f6359b3 100644
--- a/tests/regression/19-ghost-witness/02-empire-detect.t
+++ b/tests/regression/19-ghost-witness/02-empire-detect.t
@@ -12,8 +12,8 @@ The ghost invariants from the witness are confirmed.
 
 Both witness ghosts are recognized as phase ghosts.
 
-  $ grep -E "phaseGhost: global ghost_a is only accessed by unique thread .* and is only ever increased by one" 02-empire-detect.out | sed -E 's/unique thread .*/unique thread <tid> and is only ever increased by one/'
-  [Info][Witness] phaseGhost: global ghost_a is only accessed by unique thread <tid> and is only ever increased by one
+  $ grep -E "phaseGhost: global ghost_a is only accessed by unique thread .* and is monotonically increased to known bounds" 02-empire-detect.out | sed -E 's/unique thread .*/unique thread <tid> and is monotonically increased to known bounds/'
+  [Info][Witness] phaseGhost: global ghost_a is only accessed by unique thread <tid> and is monotonically increased to known bounds
 
-  $ grep -E "phaseGhost: global ghost_b is only accessed by unique thread .* and is only ever increased by one" 02-empire-detect.out | sed -E 's/unique thread .*/unique thread <tid> and is only ever increased by one/'
-  [Info][Witness] phaseGhost: global ghost_b is only accessed by unique thread <tid> and is only ever increased by one
+  $ grep -E "phaseGhost: global ghost_b is only accessed by unique thread .* and is monotonically increased to known bounds" 02-empire-detect.out | sed -E 's/unique thread .*/unique thread <tid> and is monotonically increased to known bounds/'
+  [Info][Witness] phaseGhost: global ghost_b is only accessed by unique thread <tid> and is monotonically increased to known bounds
diff --git a/tests/regression/19-ghost-witness/03-phase-ghost-matrix.c b/tests/regression/19-ghost-witness/03-phase-ghost-matrix.c
index 88ac104f0a..f14053e469 100644
--- a/tests/regression/19-ghost-witness/03-phase-ghost-matrix.c
+++ b/tests/regression/19-ghost-witness/03-phase-ghost-matrix.c
@@ -5,15 +5,15 @@
 extern int __VERIFIER_nondet_int(void);
 
 int ghost_a = 0; // phase ghost: accessed only by main and incremented by 1.
-int ghost_b = 0; // not a phase ghost: accessed only by main, but assigned a constant not equal to old + 1.
+int ghost_b = 0; // phase ghost: accessed only by main and updated from known constant 0 to 5.
 int ghost_c = 0; // phase ghost: accessed only by main and updated syntactically as 1 + ghost_c.
-int ghost_d = 0; // not a phase ghost: accessed only by main, but incremented by 2.
+int ghost_d = 0; // phase ghost: accessed only by main and incremented by 2.
 int ghost_e = 0; // not a phase ghost: accessed only by main, but increment amount is nondeterministic.
 int ghost_f = 0; // not exercised: never accessed in this test.
 int ghost_g = 0; // not a phase ghost: incremented by both main and a different unique worker thread.
 int ghost_h = 0; // not a phase ghost: incremented by a non-unique thread id.
 int ghost_i = 0; // phase ghost: accessed only by one unique worker thread and incremented by 1.
-int ghost_j = 0; // not a phase ghost: accessed only by one unique worker thread, but assigned 7.
+int ghost_j = 0; // phase ghost: accessed only by one unique worker thread and updated from known constant 0 to 7.
 int ghost_k = 0; // phase ghost: accessed only by one unique worker thread and incremented by 1 twice.
 int ghost_l = 0; // not a phase ghost: accessed only by one unique worker thread, but decremented.
 int ghost_m = 0; // not a phase ghost: incremented by both main and a different unique worker thread.
@@ -21,11 +21,11 @@ int ghost_n = 0; // not a phase ghost: updated by 0, so it is not an increment b
 int ghost_o = 0; // not a phase ghost: updated by the constant expression 1 - 1, which is not +1.
 int ghost_p = 0; // not a phase ghost: assigned by a non-unique thread id.
 int ghost_q = 4; // phase ghost: accessed only by main and updated from known constant 4 to 5.
-int ghost_r = 4; // not a phase ghost: accessed only by main, but updated from 4 to 6.
+int ghost_r = 4; // phase ghost: accessed only by main and updated from 4 to 6.
 int ghost_s = 0; // not exercised: never accessed in this test.
 int ghost_t = 0; // not exercised: never accessed in this test.
 int ghost_u = 0; // phase ghost: main first sets it from 0 to 1, then increments it by 1.
-int ghost_v = 0; // not a phase ghost: main sets it from 0 to 2.
+int ghost_v = 0; // phase ghost: main sets it from 0 to 2.
 int ghost_w = 0; // phase ghost: worker_unique sets it from 0 to 1.
 int ghost_x = 0; // not a phase ghost: incremented by a non-unique thread id.
 int ghost_y = 0; // phase ghost: accessed only by main and incremented by 1 twice.
diff --git a/tests/regression/19-ghost-witness/03-phase-ghost-matrix.t b/tests/regression/19-ghost-witness/03-phase-ghost-matrix.t
index 83ff5c7b3f..a055897869 100644
--- a/tests/regression/19-ghost-witness/03-phase-ghost-matrix.t
+++ b/tests/regression/19-ghost-witness/03-phase-ghost-matrix.t
@@ -2,29 +2,37 @@ Run `phaseGhost` on a matrix of ghost variables covering the main cases.
 
   $ goblint --set ana.activated[+] phaseGhost --enable warn.deterministic --set lib.activated[+] sv-comp --set witness.yaml.extraGhosts[+] ghost_a --set witness.yaml.extraGhosts[+] ghost_b --set witness.yaml.extraGhosts[+] ghost_c --set witness.yaml.extraGhosts[+] ghost_d --set witness.yaml.extraGhosts[+] ghost_e --set witness.yaml.extraGhosts[+] ghost_f --set witness.yaml.extraGhosts[+] ghost_g --set witness.yaml.extraGhosts[+] ghost_h --set witness.yaml.extraGhosts[+] ghost_i --set witness.yaml.extraGhosts[+] ghost_j --set witness.yaml.extraGhosts[+] ghost_k --set witness.yaml.extraGhosts[+] ghost_l --set witness.yaml.extraGhosts[+] ghost_m --set witness.yaml.extraGhosts[+] ghost_n --set witness.yaml.extraGhosts[+] ghost_o --set witness.yaml.extraGhosts[+] ghost_p --set witness.yaml.extraGhosts[+] ghost_q --set witness.yaml.extraGhosts[+] ghost_r --set witness.yaml.extraGhosts[+] ghost_s --set witness.yaml.extraGhosts[+] ghost_t --set witness.yaml.extraGhosts[+] ghost_u --set witness.yaml.extraGhosts[+] ghost_v --set witness.yaml.extraGhosts[+] ghost_w --set witness.yaml.extraGhosts[+] ghost_x --set witness.yaml.extraGhosts[+] ghost_y --set colors never 03-phase-ghost-matrix.c > phase-ghost-matrix.out 2>&1
 
-Unique-thread and increment-by-one successes are reported.
+Unique-thread and monotone bounded successes are reported.
 
-  $ grep -E "phaseGhost: global ghost_a is only accessed by unique thread .* and is only ever increased by one" phase-ghost-matrix.out | sed -E 's/unique thread .*/unique thread <tid> and is only ever increased by one/'
-  [Info][Witness] phaseGhost: global ghost_a is only accessed by unique thread <tid> and is only ever increased by one
+  $ grep -E "phaseGhost: global ghost_a is only accessed by unique thread .* and is monotonically increased to known bounds" phase-ghost-matrix.out | sed -E 's/unique thread .*/unique thread <tid> and is monotonically increased to known bounds/'
+  [Info][Witness] phaseGhost: global ghost_a is only accessed by unique thread <tid> and is monotonically increased to known bounds
 
-  $ grep -E "phaseGhost: global ghost_i is only accessed by unique thread .* and is only ever increased by one" phase-ghost-matrix.out | sed -E 's/unique thread .*/unique thread <tid> and is only ever increased by one/'
-  [Info][Witness] phaseGhost: global ghost_i is only accessed by unique thread <tid> and is only ever increased by one
+  $ grep -E "phaseGhost: global ghost_i is only accessed by unique thread .* and is monotonically increased to known bounds" phase-ghost-matrix.out | sed -E 's/unique thread .*/unique thread <tid> and is monotonically increased to known bounds/'
+  [Info][Witness] phaseGhost: global ghost_i is only accessed by unique thread <tid> and is monotonically increased to known bounds
 
 Constant-folding from known ghost values is used for non-syntactic `+1` cases too.
 
-  $ grep -E "phaseGhost: global ghost_q is only accessed by unique thread .* and is only ever increased by one" phase-ghost-matrix.out | sed -E 's/unique thread .*/unique thread <tid> and is only ever increased by one/'
-  [Info][Witness] phaseGhost: global ghost_q is only accessed by unique thread <tid> and is only ever increased by one
+  $ grep -E "phaseGhost: global ghost_q is only accessed by unique thread .* and is monotonically increased to known bounds" phase-ghost-matrix.out | sed -E 's/unique thread .*/unique thread <tid> and is monotonically increased to known bounds/'
+  [Info][Witness] phaseGhost: global ghost_q is only accessed by unique thread <tid> and is monotonically increased to known bounds
 
-Unique-thread accesses with non-`+1` updates are rejected.
+Unique-thread accesses with bounded jumps larger than one are accepted.
 
-  $ grep -E "phaseGhost: global ghost_b is only accessed by unique thread .* but is not only ever increased by one" phase-ghost-matrix.out | sed -E 's/unique thread .* but/unique thread <tid>, but/'
-  [Warning][Witness] phaseGhost: global ghost_b is only accessed by unique thread <tid>, but is not only ever increased by one
+  $ grep -E "phaseGhost: global ghost_b is only accessed by unique thread .* and is monotonically increased to known bounds" phase-ghost-matrix.out | sed -E 's/unique thread .*/unique thread <tid> and is monotonically increased to known bounds/'
+  [Info][Witness] phaseGhost: global ghost_b is only accessed by unique thread <tid> and is monotonically increased to known bounds
 
-  $ grep -E "phaseGhost: global ghost_d is only accessed by unique thread .* but is not only ever increased by one" phase-ghost-matrix.out | sed -E 's/unique thread .* but/unique thread <tid>, but/'
-  [Warning][Witness] phaseGhost: global ghost_d is only accessed by unique thread <tid>, but is not only ever increased by one
+  $ grep -E "phaseGhost: global ghost_d is only accessed by unique thread .* and is monotonically increased to known bounds" phase-ghost-matrix.out | sed -E 's/unique thread .*/unique thread <tid> and is monotonically increased to known bounds/'
+  [Info][Witness] phaseGhost: global ghost_d is only accessed by unique thread <tid> and is monotonically increased to known bounds
 
-  $ grep -E "phaseGhost: global ghost_r is only accessed by unique thread .* but is not only ever increased by one" phase-ghost-matrix.out | sed -E 's/unique thread .* but/unique thread <tid>, but/'
-  [Warning][Witness] phaseGhost: global ghost_r is only accessed by unique thread <tid>, but is not only ever increased by one
+  $ grep -E "phaseGhost: global ghost_r is only accessed by unique thread .* and is monotonically increased to known bounds" phase-ghost-matrix.out | sed -E 's/unique thread .*/unique thread <tid> and is monotonically increased to known bounds/'
+  [Info][Witness] phaseGhost: global ghost_r is only accessed by unique thread <tid> and is monotonically increased to known bounds
+
+Unique-thread accesses with unknown or non-increasing updates are rejected.
+
+  $ grep -E "phaseGhost: global ghost_e is only accessed by unique thread .* but is not monotonically increased to known bounds" phase-ghost-matrix.out | sed -E 's/unique thread .* but/unique thread <tid>, but/'
+  [Warning][Witness] phaseGhost: global ghost_e is only accessed by unique thread <tid>, but is not monotonically increased to known bounds
+
+  $ grep -E "phaseGhost: global ghost_n is only accessed by unique thread .* but is not monotonically increased to known bounds" phase-ghost-matrix.out | sed -E 's/unique thread .* but/unique thread <tid>, but/'
+  [Warning][Witness] phaseGhost: global ghost_n is only accessed by unique thread <tid>, but is not monotonically increased to known bounds
 
 Accesses from multiple unique threads are rejected.
 
diff --git a/tests/regression/19-ghost-witness/05-empire-detect-bounds.t b/tests/regression/19-ghost-witness/05-empire-detect-bounds.t
index ef3c4a3be5..a13e048f75 100644
--- a/tests/regression/19-ghost-witness/05-empire-detect-bounds.t
+++ b/tests/regression/19-ghost-witness/05-empire-detect-bounds.t
@@ -5,8 +5,8 @@ Run witness validation with `phaseGhost` on the empire example and confirm the e
     live: 16
     dead: 0
     total lines: 16
-  [Info][Witness] phaseGhost: global ghost_a is only accessed by unique thread [main, fun@05-empire-detect-bounds.c:27:5-27:51] and is only ever increased by one
-  [Info][Witness] phaseGhost: global ghost_b is only accessed by unique thread [main] and is only ever increased by one
+  [Info][Witness] phaseGhost: global ghost_a is only accessed by unique thread [main, fun@05-empire-detect-bounds.c:27:5-27:51] and is monotonically increased to known bounds
+  [Info][Witness] phaseGhost: global ghost_b is only accessed by unique thread [main] and is monotonically increased to known bounds
   [Info][Witness] witness validation summary:
     confirmed: 3
     unconfirmed: 0
diff --git a/tests/regression/19-ghost-witness/07-sync-double-advance.t b/tests/regression/19-ghost-witness/07-sync-double-advance.t
index 36cb021a8c..00e481a97a 100644
--- a/tests/regression/19-ghost-witness/07-sync-double-advance.t
+++ b/tests/regression/19-ghost-witness/07-sync-double-advance.t
@@ -8,7 +8,7 @@ strong because the spawned worker may already have reached the third phase.
     dead: 0
     total lines: 9
   [Warning][Witness] invariant unconfirmed: ghost_a == 0 || ghost_a == 1 (07-sync-double-advance.c:17:5)
-  [Info][Witness] phaseGhost: global ghost_a is only accessed by unique thread [main, fun@07-sync-double-advance.c:15:5-15:51] and is only ever increased by one
+  [Info][Witness] phaseGhost: global ghost_a is only accessed by unique thread [main, fun@07-sync-double-advance.c:15:5-15:51] and is monotonically increased to known bounds
   [Info][Witness] witness validation summary:
     confirmed: 0
     unconfirmed: 1
diff --git a/tests/regression/19-ghost-witness/08-sync-mutex-advance.t b/tests/regression/19-ghost-witness/08-sync-mutex-advance.t
index a3159029a4..9d3a0cfa30 100644
--- a/tests/regression/19-ghost-witness/08-sync-mutex-advance.t
+++ b/tests/regression/19-ghost-witness/08-sync-mutex-advance.t
@@ -6,7 +6,7 @@ inside the same mutex which main holds at the checked statement.
     live: 12
     dead: 0
     total lines: 12
-  [Info][Witness] phaseGhost: global ghost_a is only accessed by unique thread [main, fun@08-sync-mutex-advance.c:21:5-21:51] and is only ever increased by one
+  [Info][Witness] phaseGhost: global ghost_a is only accessed by unique thread [main, fun@08-sync-mutex-advance.c:21:5-21:51] and is monotonically increased to known bounds
   [Info][Witness] witness validation summary:
     confirmed: 1
     unconfirmed: 0
diff --git a/tests/regression/19-ghost-witness/09-sync-copy-under-mutex.t b/tests/regression/19-ghost-witness/09-sync-copy-under-mutex.t
index 917b51af97..8da08308ff 100644
--- a/tests/regression/19-ghost-witness/09-sync-copy-under-mutex.t
+++ b/tests/regression/19-ghost-witness/09-sync-copy-under-mutex.t
@@ -8,8 +8,8 @@ because ghost_a is accessed by multiple unique threads.
     live: 13
     dead: 0
     total lines: 13
-  [Warning][Witness] phaseGhost: global ghost_b is only accessed by unique thread [main], but is not only ever increased by one
-  [Info][Witness] phaseGhost: global ghost_a is only accessed by unique thread [main, fun@09-sync-copy-under-mutex.c:20:5-20:51] and is only ever increased by one
+  [Warning][Witness] phaseGhost: global ghost_b is only accessed by unique thread [main], but is not monotonically increased to known bounds
+  [Info][Witness] phaseGhost: global ghost_a is only accessed by unique thread [main, fun@09-sync-copy-under-mutex.c:20:5-20:51] and is monotonically increased to known bounds
   [Info][Witness] witness validation summary:
     confirmed: 1
     unconfirmed: 0
diff --git a/tests/regression/19-ghost-witness/10-malloc-phase.t b/tests/regression/19-ghost-witness/10-malloc-phase.t
index e2d65c09b4..7cac2a6105 100644
--- a/tests/regression/19-ghost-witness/10-malloc-phase.t
+++ b/tests/regression/19-ghost-witness/10-malloc-phase.t
@@ -7,8 +7,8 @@ Check that the phase propagation also happens for memory that is dynamically all
     dead: 0
     total lines: 20
   [Warning][Witness] invariant unconfirmed: *published == 10 (10-malloc-phase.c:46:5)
-  [Info][Witness] phaseGhost: global ghost_a is only accessed by unique thread [main] and is only ever increased by one
-  [Info][Witness] phaseGhost: global ghost_b is only accessed by unique thread [main] and is only ever increased by one
+  [Info][Witness] phaseGhost: global ghost_a is only accessed by unique thread [main] and is monotonically increased to known bounds
+  [Info][Witness] phaseGhost: global ghost_b is only accessed by unique thread [main] and is monotonically increased to known bounds
   [Info][Witness] witness validation summary:
     confirmed: 0
     unconfirmed: 1
diff --git a/tests/regression/19-ghost-witness/11-empire-detect-bounds-malloc.t b/tests/regression/19-ghost-witness/11-empire-detect-bounds-malloc.t
index 7917918c85..559ecb5c58 100644
--- a/tests/regression/19-ghost-witness/11-empire-detect-bounds-malloc.t
+++ b/tests/regression/19-ghost-witness/11-empire-detect-bounds-malloc.t
@@ -6,8 +6,8 @@ as a global pointer to a dynamically allocated integer.
     live: 17
     dead: 0
     total lines: 17
-  [Info][Witness] phaseGhost: global ghost_a is only accessed by unique thread [main, fun@11-empire-detect-bounds-malloc.c:30:5-30:51] and is only ever increased by one
-  [Info][Witness] phaseGhost: global ghost_b is only accessed by unique thread [main] and is only ever increased by one
+  [Info][Witness] phaseGhost: global ghost_a is only accessed by unique thread [main, fun@11-empire-detect-bounds-malloc.c:30:5-30:51] and is monotonically increased to known bounds
+  [Info][Witness] phaseGhost: global ghost_b is only accessed by unique thread [main] and is monotonically increased to known bounds
   [Info][Witness] witness validation summary:
     confirmed: 3
     unconfirmed: 0
diff --git a/tests/regression/19-ghost-witness/12-non-phase-ghost-propagation.t b/tests/regression/19-ghost-witness/12-non-phase-ghost-propagation.t
index 88d096c355..8b1f87e0d0 100644
--- a/tests/regression/19-ghost-witness/12-non-phase-ghost-propagation.t
+++ b/tests/regression/19-ghost-witness/12-non-phase-ghost-propagation.t
@@ -7,9 +7,9 @@ would unsoundly confirm the invariant.
     live: 19
     dead: 0
     total lines: 19
-  [Warning][Witness] phaseGhost: global ghost_non_phase is only accessed by unique thread [main], but is not only ever increased by one
+  [Warning][Witness] phaseGhost: global ghost_non_phase is only accessed by unique thread [main], but is not monotonically increased to known bounds
   [Warning][Witness] invariant unconfirmed: ghost_non_phase == 10 (12-non-phase-ghost-propagation.c:45:5)
-  [Info][Witness] phaseGhost: global ghost_phase is only accessed by unique thread [main, fun@12-non-phase-ghost-propagation.c:31:5-31:51] and is only ever increased by one
+  [Info][Witness] phaseGhost: global ghost_phase is only accessed by unique thread [main, fun@12-non-phase-ghost-propagation.c:31:5-31:51] and is monotonically increased to known bounds
   [Info][Witness] witness validation summary:
     confirmed: 0
     unconfirmed: 1
diff --git a/tests/regression/19-ghost-witness/12-non-phase-ghost-propagation.yml b/tests/regression/19-ghost-witness/12-non-phase-ghost-propagation.yml
index 5eeade0cdf..23b8c43985 100644
--- a/tests/regression/19-ghost-witness/12-non-phase-ghost-propagation.yml
+++ b/tests/regression/19-ghost-witness/12-non-phase-ghost-propagation.yml
@@ -44,7 +44,7 @@
         function: main
       updates:
       - variable: ghost_non_phase
-        value: "7"
+        value: "ghost_non_phase + 0"
         format: c_expression
     - location:
         file_name: 12-non-phase-ghost-propagation.c