diff --git a/src/arg/argTools.ml b/src/arg/argTools.ml
index a220120912..6d91fc3843 100644
--- a/src/arg/argTools.ml
+++ b/src/arg/argTools.ml
@@ -137,19 +137,6 @@ struct
       | Statement stmt  -> Printf.sprintf "s%d(%d)[%s]" stmt.sid c_tag i_str
       | Function f      -> Printf.sprintf "ret%d%s(%d)[%s]" f.svar.vid f.svar.vname c_tag i_str
       | FunctionEntry f -> Printf.sprintf "fun%d%s(%d)[%s]" f.svar.vid f.svar.vname c_tag i_str
-
-    (* TODO: less hacky way (without ask_indices) to move node *)
-    let is_live (n, c, i) = not (Spec.D.is_bot (get (n, c)))
-    let move_opt (n, c, i) to_n =
-      match ask_indices (to_n, c) with
-      | [] -> None
-      | [to_i] ->
-        let to_node = (to_n, c, to_i) in
-        BatOption.filter is_live (Some to_node)
-      | _ :: _ :: _ ->
-        failwith "Node.move_opt: ambiguous moved index"
-    let equal_node_context (n1, c1, i1) (n2, c2, i2) =
-      EQSys.LVar.equal (n1, c1) (n2, c2)
   end
 
   module NHT = BatHashtbl.Make (Node)
diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index f92f531f0d..c41a442f10 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -12,14 +12,11 @@ sig
   val context_id: t -> int
   val path_id: t -> int
   val to_string: t -> string
-
-  val move_opt: t -> MyCFG.node -> t option
-  val equal_node_context: t -> t -> bool
 end
 
 module type Edge =
 sig
-  type t
+  type t [@@deriving eq, ord]
 
   val embed: MyCFG.edge -> t
   val to_string: t -> string
@@ -27,7 +24,7 @@ end
 
 module CFGEdge: Edge with type t = MyCFG.edge =
 struct
-  type t = edge
+  type t = Edge.t [@@deriving eq, ord]
 
   let embed e = e
   let to_string e = GobPretty.sprint Edge.pretty_plain e
@@ -102,7 +99,7 @@ end
 
 module InlineEdge: Edge with type t = inline_edge =
 struct
-  type t = inline_edge
+  type t = inline_edge [@@deriving eq, ord]
 
   let embed e = CFGEdge e
   let to_string e = InlineEdgePrintable.show e
@@ -130,15 +127,6 @@ struct
     nl
     |> List.map Node.to_string
     |> String.concat "@"
-
-  let move_opt nl to_node =
-    let open GobOption.Syntax in
-    match nl with
-    | [] -> None
-    | n :: stack ->
-      let+ to_n = Node.move_opt n to_node in
-      to_n :: stack
-  let equal_node_context _ _ = failwith "StackNode: equal_node_context"
 end
 
 module Stack (Arg: S with module Edge = InlineEdge):
@@ -265,16 +253,19 @@ struct
     end
 end
 
+type cfg_path = (MyCFG.edge * MyCFG.node) list
 
 module type SIntra =
 sig
-  val next: MyCFG.node -> (MyCFG.edge * MyCFG.node) list
+  val next: MyCFG.node -> (MyCFG.edge * MyCFG.node * cfg_path list) list
+  (** @return Also the original CFG paths corresponding to the step. *)
 end
 
 module type SIntraOpt =
 sig
   include SIntra
-  val next_opt: MyCFG.node -> ((MyCFG.edge * MyCFG.node) list) option
+  val next_opt: MyCFG.node -> ((MyCFG.edge * MyCFG.node * cfg_path list) list) option
+  (** @return Also the original CFG paths corresponding to the step. *)
 end
 
 module CfgIntra (Cfg:CfgForward): SIntraOpt =
@@ -283,51 +274,38 @@ struct
     let open GobList.Syntax in
     let* (es, to_n) = Cfg.next node in
     let+ (_, e) = es in
-    (e, to_n)
+    (e, to_n, [[(e, to_n)]])
   let next_opt _ = None
 end
 
-let partition_if_next if_next_n =
-  (* TODO: refactor, check extra edges for error *)
-  let test_next b = List.find (function
-      | (Test (_, b'), _) when b = b' -> true
-      | (_, _) -> false
-    ) if_next_n
+let cartesian_concat_paths (ps : cfg_path list) (qs : cfg_path list) : cfg_path list = List.concat_map (fun p -> List.map (fun q -> p @ q) qs) ps
+
+let partition_if_next if_next =
+  let (if_next_trues, if_next_falses) = List.partition (function
+      | (Test (_, b), _, _) -> b
+      | (_, _, _) -> failwith "partition_if_next: not Test edge"
+    ) if_next
   in
-  (* assert (List.length if_next <= 2); *)
-  match test_next true, test_next false with
-  | (Test (e_true, true), if_true_next_n), (Test (e_false, false), if_false_next_n) when Basetype.CilExp.equal e_true e_false ->
-    (e_true, if_true_next_n, if_false_next_n)
-  | _, _ -> failwith "partition_if_next: bad branches"
+  match if_next_trues, if_next_falses with
+  | [(Test (e_true, true), if_true_next_n, if_true_next_ps)], [(Test (e_false, false), if_false_next_n, if_false_next_ps)] when Basetype.CilExp.equal e_true e_false ->
+    (e_true, (if_true_next_n, if_true_next_ps), (if_false_next_n, if_false_next_ps))
+  | _, _ ->
+    (* This fails due to any of the following:
+       - Either true or false branch is missing.
+       - Either true or false branch has multiple different exps or nodes (same exp, branch and node should only occur once by construction/assumption).
+       - True and false branch have different exps. *)
+    failwith "partition_if_next: bad branches"
 
 module UnCilLogicIntra (Arg: SIntraOpt): SIntraOpt =
 struct
   open Cil
-  (* TODO: questionable (=) and (==) use here *)
-
-  let is_equiv_stmtkind sk1 sk2 = match sk1, sk2 with
-    | Instr is1, Instr is2 -> GobList.equal (=) is1 is2
-    | Return _, Return _ -> sk1 = sk2
-    | _, _ -> false (* TODO: also consider others? not sure if they ever get duplicated *)
-  let is_equiv_stmt s1 s2 = is_equiv_stmtkind s1.skind s2.skind (* TODO: also consider labels *)
-  let is_equiv_node n1 n2 = match n1, n2 with
-    | Statement s1, Statement s2 -> is_equiv_stmt s1 s2
-    | _, _ -> false (* TODO: also consider FunctionEntry & Function? *)
-  let is_equiv_edge e1 e2 = match e1, e2 with
-    | Entry f1, Entry f2 -> f1 == f2 (* physical equality for fundec to avoid cycle *)
-    | Ret (exp1, f1), Ret (exp2, f2) -> exp1 = exp2 && f1 == f2 (* physical equality for fundec to avoid cycle *)
-    | _, _ -> e1 = e2
-  let rec is_equiv_chain n1 n2 =
-    Node.equal n1 n2 || (is_equiv_node n1 n2 && is_equiv_chain_next n1 n2)
-  and is_equiv_chain_next n1 n2 = match Arg.next n1, Arg.next n2 with
-    | [(e1, to_n1)], [(e2, to_n2)] ->
-      is_equiv_edge e1 e2 && is_equiv_chain to_n1 to_n2
-    | _, _-> false
 
+  let () =
+    assert (not !Cabs2cil.allowDuplication) (* duplication makes it more annoying to detect cilling *)
 
   let rec next_opt' n = match n with
     | Statement {sid; skind=If _; _} when GobConfig.get_bool "exp.arg.uncil" ->
-      let (e, if_true_next_n,  if_false_next_n) = partition_if_next (Arg.next n) in
+      let (e, (if_true_next_n, if_true_next_ps), (if_false_next_n, if_false_next_ps)) = partition_if_next (Arg.next n) in
       (* avoid infinite recursion with sid <> sid2 in if_nondet_var *)
       (* TODO: why physical comparison if_false_next_n != n doesn't work? *)
       (* TODO: need to handle longer loops? *)
@@ -336,24 +314,24 @@ struct
         (* && *)
         | Statement {sid=sid2; skind=If _; _}, _ when sid <> sid2 && CilType.Location.equal loc (Node.location if_true_next_n) ->
           (* get e2 from edge because recursive next returns it there *)
-          let (e2, if_true_next_true_next_n, if_true_next_false_next_n) = partition_if_next (next if_true_next_n) in
-          if is_equiv_chain if_false_next_n if_true_next_false_next_n then
+          let (e2, (if_true_next_true_next_n, if_true_next_true_next_ps), (if_true_next_false_next_n, if_true_next_false_next_ps)) = partition_if_next (next if_true_next_n) in
+          if Node.equal if_false_next_n if_true_next_false_next_n then
             let exp = BinOp (LAnd, e, e2, intType) in
             Some [
-              (Test (exp, true), if_true_next_true_next_n);
-              (Test (exp, false), if_false_next_n)
+              (Test (exp, true), if_true_next_true_next_n, cartesian_concat_paths if_true_next_ps if_true_next_true_next_ps);
+              (Test (exp, false), if_true_next_false_next_n, if_false_next_ps @ cartesian_concat_paths if_true_next_ps if_true_next_false_next_ps) (* concat two different path families to same false node *)
             ]
           else
             None
         (* || *)
         | _, Statement {sid=sid2; skind=If _; _} when sid <> sid2 && CilType.Location.equal loc (Node.location if_false_next_n) ->
           (* get e2 from edge because recursive next returns it there *)
-          let (e2, if_false_next_true_next_n, if_false_next_false_next_n) = partition_if_next (next if_false_next_n) in
-          if is_equiv_chain if_true_next_n if_false_next_true_next_n then
+          let (e2, (if_false_next_true_next_n, if_false_next_true_next_ps), (if_false_next_false_next_n, if_false_next_false_next_ps)) = partition_if_next (next if_false_next_n) in
+          if Node.equal if_true_next_n if_false_next_true_next_n then
             let exp = BinOp (LOr, e, e2, intType) in
             Some [
-              (Test (exp, true), if_true_next_n);
-              (Test (exp, false), if_false_next_false_next_n)
+              (Test (exp, true), if_false_next_true_next_n, if_true_next_ps @ cartesian_concat_paths if_false_next_ps if_false_next_true_next_ps); (* concat two different path families to same true node *)
+              (Test (exp, false), if_false_next_false_next_n, cartesian_concat_paths if_false_next_ps if_false_next_false_next_ps)
             ]
           else
             None
@@ -381,14 +359,14 @@ struct
 
   let next_opt' n = match n with
     | Statement {skind=If _; _} when GobConfig.get_bool "exp.arg.uncil" ->
-      let (e_cond, if_true_next_n, if_false_next_n) = partition_if_next (Arg.next n) in
+      let (e_cond, (if_true_next_n, if_true_next_ps), (if_false_next_n, if_false_next_ps)) = partition_if_next (Arg.next n) in
       let loc = Node.location n in
       if CilType.Location.equal (Node.location if_true_next_n) loc && CilType.Location.equal (Node.location if_false_next_n) loc then
         match Arg.next if_true_next_n, Arg.next if_false_next_n with
-        | [(Assign (v_true, e_true), if_true_next_next_n)], [(Assign (v_false, e_false), if_false_next_next_n)] when v_true = v_false && Node.equal if_true_next_next_n if_false_next_next_n ->
+        | [(Assign (v_true, e_true), if_true_next_next_n, if_true_next_next_ps)], [(Assign (v_false, e_false), if_false_next_next_n, if_false_next_next_ps)] when v_true = v_false && Node.equal if_true_next_next_n if_false_next_next_n ->
           let exp = ternary e_cond e_true e_false in
           Some [
-            (Assign (v_true, exp), if_true_next_next_n)
+            (Assign (v_true, exp), if_true_next_next_n, cartesian_concat_paths if_true_next_ps if_true_next_next_ps @ cartesian_concat_paths if_false_next_ps if_false_next_next_ps) (* concat two different path families with same variable to same node *)
           ]
         | _, _ -> None
       else
@@ -407,14 +385,30 @@ module Intra (ArgIntra: SIntraOpt) (Arg: S):
 struct
   include Arg
 
+  (** Starting from ARG node [node], follow CFG path [p] to the resulting ARG node.
+      Returns multiple ARG nodes if ARG contains path-sensitivity splits on the same CFG path. *)
+  let rec follow node p =
+    let open GobList.Syntax in
+    match p with
+    | [] -> [node]
+    | (e, to_n) :: p' ->
+      let* (_, node') = List.filter (fun (e', to_node) ->
+          Edge.equal (Edge.embed e) e' && Node0.equal to_n (Node.cfgnode to_node)
+        ) (Arg.next node)
+      in
+      follow node' p'
+
   let next node =
-    let open GobOption.Syntax in
+    let open GobList.Syntax in
     match ArgIntra.next_opt (Node.cfgnode node) with
     | None -> Arg.next node
     | Some next ->
       next
-      |> BatList.filter_map (fun (e, to_n) ->
-          let+ to_node = Node.move_opt node to_n in
+      |> BatList.concat_map (fun (e, to_n, p) ->
+          let* p in
+          let+ to_node = follow node p in
+          assert (Node0.equal to_n (Node.cfgnode to_node)); (* should always hold by follow filter above *)
           (Edge.embed e, to_node)
         )
+      |> BatList.unique_cmp ~cmp:[%ord: Edge.t * Node.t] (* after following paths, there may be duplicates because same ARG node can be reached via same ARG edge via multiple uncilled CFG paths *) (* TODO: avoid generating duplicates in the first place? *)
 end
diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml
index 635edb8ab7..452d0297a5 100644
--- a/src/common/util/cilfacade.ml
+++ b/src/common/util/cilfacade.ml
@@ -90,7 +90,7 @@ let init () =
   (* lineDirectiveStyle := None; *)
   RmUnused.keepUnused := true;
   print_CIL_Input := true;
-  Cabs2cil.allowDuplication := false;
+  Cabs2cil.allowDuplication := false; (* needed for ARG uncilling, maybe something else as well? *)
   Cabs2cil.silenceLongDoubleWarning := true;
   Cabs2cil.addLoopConditionLabels := true
 
diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous1.c b/tests/sv-comp/cfg/uncil/and_ambiguous1.c
new file mode 100644
index 0000000000..d35441c02c
--- /dev/null
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous1.c
@@ -0,0 +1,13 @@
+#include <goblint.h>
+
+int main() {
+    int a, b;
+
+    __goblint_split_begin(a);
+    if (a && b) {
+        return 1;
+    }
+    else {
+        return 0;
+    }
+}
diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous1.expected b/tests/sv-comp/cfg/uncil/and_ambiguous1.expected
new file mode 100644
index 0000000000..560abd05c3
--- /dev/null
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous1.expected
@@ -0,0 +1,27 @@
+                             ┌──────────────────────────────────┐
+                             │                _                 │
+                             └──────────────────────────────────┘
+                               │
+                               │ Entry main
+                               ▼
+                             ┌──────────────────────────────────┐
+                             │                _                 │
+                             └──────────────────────────────────┘
+                               │
+                               │ Proc '__goblint_split_begin(a)'
+                               ▼
+┌───┐  Test (a && b,false)   ┌──────────────────────────────────┐  Test (a && b,false)   ┌───┐
+│ _ │ ◀───────────────────── │                _                 │ ─────────────────────▶ │ _ │
+└───┘                        └──────────────────────────────────┘                        └───┘
+  │                            │                                                           │
+  │                            │ Test (a && b,true)                                        │
+  │                            ▼                                                           │
+  │                          ┌──────────────────────────────────┐                          │
+  │                          │                _                 │                          │
+  │                          └──────────────────────────────────┘                          │
+  │                            │                                                           │
+  │                            │ Ret (Some 1, main)                                        │
+  │                            ▼                                                           │
+  │   Ret (Some 0, main)     ┌──────────────────────────────────┐  Ret (Some 0, main)      │
+  └────────────────────────▶ │                _                 │ ◀────────────────────────┘
+                             └──────────────────────────────────┘
diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous2.c b/tests/sv-comp/cfg/uncil/and_ambiguous2.c
new file mode 100644
index 0000000000..058ccee377
--- /dev/null
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous2.c
@@ -0,0 +1,13 @@
+#include <goblint.h>
+
+int main() {
+    int a, b;
+
+    __goblint_split_begin(b);
+    if (a && b) {
+        return 1;
+    }
+    else {
+        return 0;
+    }
+}
diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous2.expected b/tests/sv-comp/cfg/uncil/and_ambiguous2.expected
new file mode 100644
index 0000000000..1cbc9466a2
--- /dev/null
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous2.expected
@@ -0,0 +1,27 @@
+                             ┌──────────────────────────────────┐
+                             │                _                 │
+                             └──────────────────────────────────┘
+                               │
+                               │ Entry main
+                               ▼
+                             ┌──────────────────────────────────┐
+                             │                _                 │
+                             └──────────────────────────────────┘
+                               │
+                               │ Proc '__goblint_split_begin(b)'
+                               ▼
+┌───┐  Test (a && b,false)   ┌──────────────────────────────────┐  Test (a && b,false)   ┌───┐
+│ _ │ ◀───────────────────── │                _                 │ ─────────────────────▶ │ _ │
+└───┘                        └──────────────────────────────────┘                        └───┘
+  │                            │                                                           │
+  │                            │ Test (a && b,true)                                        │
+  │                            ▼                                                           │
+  │                          ┌──────────────────────────────────┐                          │
+  │                          │                _                 │                          │
+  │                          └──────────────────────────────────┘                          │
+  │                            │                                                           │
+  │                            │ Ret (Some 1, main)                                        │
+  │                            ▼                                                           │
+  │   Ret (Some 0, main)     ┌──────────────────────────────────┐  Ret (Some 0, main)      │
+  └────────────────────────▶ │                _                 │ ◀────────────────────────┘
+                             └──────────────────────────────────┘
diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous_partition1.c b/tests/sv-comp/cfg/uncil/and_ambiguous_partition1.c
new file mode 100644
index 0000000000..5115845160
--- /dev/null
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous_partition1.c
@@ -0,0 +1,13 @@
+#include <goblint.h>
+
+int main() {
+    int a, b = 0, c;
+
+    __goblint_split_begin(a);
+    if (a && b && c) {
+        return 1;
+    }
+    else {
+        return 0;
+    }
+}
diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous_partition1.expected b/tests/sv-comp/cfg/uncil/and_ambiguous_partition1.expected
new file mode 100644
index 0000000000..8c1a83b95a
--- /dev/null
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous_partition1.expected
@@ -0,0 +1,33 @@
+                                    ┌──────────────────────────────────┐
+                                    │                _                 │
+                                    └──────────────────────────────────┘
+                                      │
+                                      │ Entry main
+                                      ▼
+                                    ┌──────────────────────────────────┐
+                                    │                _                 │
+                                    └──────────────────────────────────┘
+                                      │
+                                      │ Assign 'b = 0'
+                                      ▼
+                                    ┌──────────────────────────────────┐
+                                    │                _                 │
+                                    └──────────────────────────────────┘
+                                      │
+                                      │ Proc '__goblint_split_begin(a)'
+                                      ▼
+┌───┐  Test (a && (b && c),false)   ┌──────────────────────────────────┐
+│ _ │ ◀──────────────────────────── │                _                 │
+└───┘                               └──────────────────────────────────┘
+  │                                   │
+  │                                   │ Test (a && (b && c),false)
+  │                                   ▼
+  │                                 ┌──────────────────────────────────┐
+  │                                 │                _                 │
+  │                                 └──────────────────────────────────┘
+  │                                   │
+  │                                   │ Ret (Some 0, main)
+  │                                   ▼
+  │   Ret (Some 0, main)            ┌──────────────────────────────────┐
+  └───────────────────────────────▶ │                _                 │
+                                    └──────────────────────────────────┘
diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous_partition2.c b/tests/sv-comp/cfg/uncil/and_ambiguous_partition2.c
new file mode 100644
index 0000000000..a1b3668a66
--- /dev/null
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous_partition2.c
@@ -0,0 +1,13 @@
+#include <goblint.h>
+
+int main() {
+    int a, b = 1, c;
+
+    __goblint_split_begin(a);
+    if (a && b && c) {
+        return 1;
+    }
+    else {
+        return 0;
+    }
+}
diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous_partition2.expected b/tests/sv-comp/cfg/uncil/and_ambiguous_partition2.expected
new file mode 100644
index 0000000000..4d44cd4454
--- /dev/null
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous_partition2.expected
@@ -0,0 +1,33 @@
+                                    ┌──────────────────────────────────┐
+                                    │                _                 │
+                                    └──────────────────────────────────┘
+                                      │
+                                      │ Entry main
+                                      ▼
+                                    ┌──────────────────────────────────┐
+                                    │                _                 │
+                                    └──────────────────────────────────┘
+                                      │
+                                      │ Assign 'b = 1'
+                                      ▼
+                                    ┌──────────────────────────────────┐
+                                    │                _                 │
+                                    └──────────────────────────────────┘
+                                      │
+                                      │ Proc '__goblint_split_begin(a)'
+                                      ▼
+┌───┐  Test (a && (b && c),false)   ┌──────────────────────────────────┐  Test (a && (b && c),false)   ┌───┐
+│ _ │ ◀──────────────────────────── │                _                 │ ────────────────────────────▶ │ _ │
+└───┘                               └──────────────────────────────────┘                               └───┘
+  │                                   │                                                                  │
+  │                                   │ Test (a && (b && c),true)                                        │
+  │                                   ▼                                                                  │
+  │                                 ┌──────────────────────────────────┐                                 │
+  │                                 │                _                 │                                 │
+  │                                 └──────────────────────────────────┘                                 │
+  │                                   │                                                                  │
+  │                                   │ Ret (Some 1, main)                                               │
+  │                                   ▼                                                                  │
+  │   Ret (Some 0, main)            ┌──────────────────────────────────┐  Ret (Some 0, main)             │
+  └───────────────────────────────▶ │                _                 │ ◀───────────────────────────────┘
+                                    └──────────────────────────────────┘
diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous_partition3.c b/tests/sv-comp/cfg/uncil/and_ambiguous_partition3.c
new file mode 100644
index 0000000000..959d0dd343
--- /dev/null
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous_partition3.c
@@ -0,0 +1,13 @@
+#include <goblint.h>
+
+int main() {
+    int a, b, c = 0;
+
+    __goblint_split_begin(a);
+    if (a && b && c) {
+        return 1;
+    }
+    else {
+        return 0;
+    }
+}
diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous_partition3.expected b/tests/sv-comp/cfg/uncil/and_ambiguous_partition3.expected
new file mode 100644
index 0000000000..7a31f9703e
--- /dev/null
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous_partition3.expected
@@ -0,0 +1,33 @@
+                                    ┌──────────────────────────────────┐
+                                    │                _                 │
+                                    └──────────────────────────────────┘
+                                      │
+                                      │ Entry main
+                                      ▼
+                                    ┌──────────────────────────────────┐
+                                    │                _                 │
+                                    └──────────────────────────────────┘
+                                      │
+                                      │ Assign 'c = 0'
+                                      ▼
+                                    ┌──────────────────────────────────┐
+                                    │                _                 │
+                                    └──────────────────────────────────┘
+                                      │
+                                      │ Proc '__goblint_split_begin(a)'
+                                      ▼
+┌───┐  Test (a && (b && c),false)   ┌──────────────────────────────────┐
+│ _ │ ◀──────────────────────────── │                _                 │
+└───┘                               └──────────────────────────────────┘
+  │                                   │
+  │                                   │ Test (a && (b && c),false)
+  │                                   ▼
+  │                                 ┌──────────────────────────────────┐
+  │                                 │                _                 │
+  │                                 └──────────────────────────────────┘
+  │                                   │
+  │                                   │ Ret (Some 0, main)
+  │                                   ▼
+  │   Ret (Some 0, main)            ┌──────────────────────────────────┐
+  └───────────────────────────────▶ │                _                 │
+                                    └──────────────────────────────────┘
diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous_partition4.c b/tests/sv-comp/cfg/uncil/and_ambiguous_partition4.c
new file mode 100644
index 0000000000..5f7a958ddd
--- /dev/null
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous_partition4.c
@@ -0,0 +1,13 @@
+#include <goblint.h>
+
+int main() {
+    int a, b, c = 1;
+
+    __goblint_split_begin(a);
+    if (a && b && c) {
+        return 1;
+    }
+    else {
+        return 0;
+    }
+}
diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous_partition4.expected b/tests/sv-comp/cfg/uncil/and_ambiguous_partition4.expected
new file mode 100644
index 0000000000..01db9837f8
--- /dev/null
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous_partition4.expected
@@ -0,0 +1,33 @@
+                                    ┌──────────────────────────────────┐
+                                    │                _                 │
+                                    └──────────────────────────────────┘
+                                      │
+                                      │ Entry main
+                                      ▼
+                                    ┌──────────────────────────────────┐
+                                    │                _                 │
+                                    └──────────────────────────────────┘
+                                      │
+                                      │ Assign 'c = 1'
+                                      ▼
+                                    ┌──────────────────────────────────┐
+                                    │                _                 │
+                                    └──────────────────────────────────┘
+                                      │
+                                      │ Proc '__goblint_split_begin(a)'
+                                      ▼
+┌───┐  Test (a && (b && c),false)   ┌──────────────────────────────────┐  Test (a && (b && c),false)   ┌───┐
+│ _ │ ◀──────────────────────────── │                _                 │ ────────────────────────────▶ │ _ │
+└───┘                               └──────────────────────────────────┘                               └───┘
+  │                                   │                                                                  │
+  │                                   │ Test (a && (b && c),true)                                        │
+  │                                   ▼                                                                  │
+  │                                 ┌──────────────────────────────────┐                                 │
+  │                                 │                _                 │                                 │
+  │                                 └──────────────────────────────────┘                                 │
+  │                                   │                                                                  │
+  │                                   │ Ret (Some 1, main)                                               │
+  │                                   ▼                                                                  │
+  │   Ret (Some 0, main)            ┌──────────────────────────────────┐  Ret (Some 0, main)             │
+  └───────────────────────────────▶ │                _                 │ ◀───────────────────────────────┘
+                                    └──────────────────────────────────┘
diff --git a/tests/sv-comp/dune.inc b/tests/sv-comp/dune.inc
index 689f97ebf3..3ff8f5a872 100644
--- a/tests/sv-comp/dune.inc
+++ b/tests/sv-comp/dune.inc
@@ -12,7 +12,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -34,7 +34,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -56,7 +56,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -78,7 +78,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -100,7 +100,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -122,7 +122,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -144,7 +144,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -166,7 +166,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -188,7 +188,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -210,7 +210,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -232,7 +232,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -254,7 +254,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -276,7 +276,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -298,7 +298,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -320,7 +320,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -342,7 +342,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -364,7 +364,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -386,7 +386,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -408,7 +408,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -430,7 +430,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -452,7 +452,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -474,7 +474,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -496,7 +496,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -518,7 +518,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -540,7 +540,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -562,7 +562,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -584,7 +584,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -606,7 +606,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -628,7 +628,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -650,7 +650,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -672,7 +672,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -694,7 +694,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -716,7 +716,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -738,7 +738,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -760,7 +760,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -770,6 +770,138 @@
   (action
    (diff and3dead_true-unreach-call.expected and3dead_true-unreach-call.output))))
 
+(subdir cfg/uncil
+ (rule
+  (deps
+   (sandbox always) ; must sandbox to prevent arg.dot-s from parallel runs from interfering
+   (package goblint) ; depend on entire goblint package for svcomp21 conf
+   (:c and_ambiguous1.c)
+   (:prop %{project_root}/tests/sv-comp/unreach-call-__VERIFIER_error.prp))
+  (target and_ambiguous1.output)
+  (enabled_if %{bin-available:graph-easy})
+  (action
+   (progn
+    (ignore-outputs
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
+    (with-outputs-to %{target}
+     (run graph-easy --as=boxart arg.dot)))))
+
+ (rule
+  (alias runtest)
+  (enabled_if %{bin-available:graph-easy})
+  (action
+   (diff and_ambiguous1.expected and_ambiguous1.output))))
+
+(subdir cfg/uncil
+ (rule
+  (deps
+   (sandbox always) ; must sandbox to prevent arg.dot-s from parallel runs from interfering
+   (package goblint) ; depend on entire goblint package for svcomp21 conf
+   (:c and_ambiguous2.c)
+   (:prop %{project_root}/tests/sv-comp/unreach-call-__VERIFIER_error.prp))
+  (target and_ambiguous2.output)
+  (enabled_if %{bin-available:graph-easy})
+  (action
+   (progn
+    (ignore-outputs
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
+    (with-outputs-to %{target}
+     (run graph-easy --as=boxart arg.dot)))))
+
+ (rule
+  (alias runtest)
+  (enabled_if %{bin-available:graph-easy})
+  (action
+   (diff and_ambiguous2.expected and_ambiguous2.output))))
+
+(subdir cfg/uncil
+ (rule
+  (deps
+   (sandbox always) ; must sandbox to prevent arg.dot-s from parallel runs from interfering
+   (package goblint) ; depend on entire goblint package for svcomp21 conf
+   (:c and_ambiguous_partition1.c)
+   (:prop %{project_root}/tests/sv-comp/unreach-call-__VERIFIER_error.prp))
+  (target and_ambiguous_partition1.output)
+  (enabled_if %{bin-available:graph-easy})
+  (action
+   (progn
+    (ignore-outputs
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
+    (with-outputs-to %{target}
+     (run graph-easy --as=boxart arg.dot)))))
+
+ (rule
+  (alias runtest)
+  (enabled_if %{bin-available:graph-easy})
+  (action
+   (diff and_ambiguous_partition1.expected and_ambiguous_partition1.output))))
+
+(subdir cfg/uncil
+ (rule
+  (deps
+   (sandbox always) ; must sandbox to prevent arg.dot-s from parallel runs from interfering
+   (package goblint) ; depend on entire goblint package for svcomp21 conf
+   (:c and_ambiguous_partition2.c)
+   (:prop %{project_root}/tests/sv-comp/unreach-call-__VERIFIER_error.prp))
+  (target and_ambiguous_partition2.output)
+  (enabled_if %{bin-available:graph-easy})
+  (action
+   (progn
+    (ignore-outputs
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
+    (with-outputs-to %{target}
+     (run graph-easy --as=boxart arg.dot)))))
+
+ (rule
+  (alias runtest)
+  (enabled_if %{bin-available:graph-easy})
+  (action
+   (diff and_ambiguous_partition2.expected and_ambiguous_partition2.output))))
+
+(subdir cfg/uncil
+ (rule
+  (deps
+   (sandbox always) ; must sandbox to prevent arg.dot-s from parallel runs from interfering
+   (package goblint) ; depend on entire goblint package for svcomp21 conf
+   (:c and_ambiguous_partition3.c)
+   (:prop %{project_root}/tests/sv-comp/unreach-call-__VERIFIER_error.prp))
+  (target and_ambiguous_partition3.output)
+  (enabled_if %{bin-available:graph-easy})
+  (action
+   (progn
+    (ignore-outputs
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
+    (with-outputs-to %{target}
+     (run graph-easy --as=boxart arg.dot)))))
+
+ (rule
+  (alias runtest)
+  (enabled_if %{bin-available:graph-easy})
+  (action
+   (diff and_ambiguous_partition3.expected and_ambiguous_partition3.output))))
+
+(subdir cfg/uncil
+ (rule
+  (deps
+   (sandbox always) ; must sandbox to prevent arg.dot-s from parallel runs from interfering
+   (package goblint) ; depend on entire goblint package for svcomp21 conf
+   (:c and_ambiguous_partition4.c)
+   (:prop %{project_root}/tests/sv-comp/unreach-call-__VERIFIER_error.prp))
+  (target and_ambiguous_partition4.output)
+  (enabled_if %{bin-available:graph-easy})
+  (action
+   (progn
+    (ignore-outputs
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
+    (with-outputs-to %{target}
+     (run graph-easy --as=boxart arg.dot)))))
+
+ (rule
+  (alias runtest)
+  (enabled_if %{bin-available:graph-easy})
+  (action
+   (diff and_ambiguous_partition4.expected and_ambiguous_partition4.output))))
+
 (subdir cfg/uncil
  (rule
   (deps
@@ -782,7 +914,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -804,7 +936,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -826,7 +958,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -848,7 +980,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -870,7 +1002,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -892,7 +1024,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -914,7 +1046,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
@@ -936,7 +1068,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %{target}
      (run graph-easy --as=boxart arg.dot)))))
 
diff --git a/tests/sv-comp/gen/gen.ml b/tests/sv-comp/gen/gen.ml
index a8ad72be67..796ae7a278 100644
--- a/tests/sv-comp/gen/gen.ml
+++ b/tests/sv-comp/gen/gen.ml
@@ -19,7 +19,7 @@ let generate_rule c_dir_file =
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %%{prop} %%{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty))
+     (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %%{prop} %%{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --set ana.activated[+] expsplit))
     (with-outputs-to %%{target}
      (run graph-easy --as=boxart arg.dot)))))