From 552d6bb16f6f46139e8b6c4c235b870b1e4375bb Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Sat, 28 Jun 2025 18:52:35 +0300
Subject: [PATCH 01/73] Reintroduce some ARG related code that was removed in
 70e1be6

---
 src/witness/witness.ml | 41 +++++++++++++++++++++++++++++------------
 1 file changed, 29 insertions(+), 12 deletions(-)

diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index ffb79fc4e0..bd3123b6f4 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -87,18 +87,35 @@ struct
 
   let determine_result entrystates (module Task:Task) (spec: Svcomp.Specification.t): Svcomp.Result.t =
     let module Arg: BiArgInvariant =
-    struct
-      module Node = ArgTool.Node
-      module Edge = MyARG.InlineEdge
-      let next _ = []
-      let prev _ = []
-      let find_invariant _ = Invariant.none
-      let main_entry =
-        let lvar = WitnessUtil.find_main_entry entrystates in
-        (fst lvar, snd lvar, -1)
-      let iter_nodes f = f main_entry
-      let query _ q = Queries.Result.top q
-    end
+      (val if GobConfig.get_bool "exp.arg.enabled" then (
+           let module Arg = (val ArgTool.create entrystates) in
+           let module Arg =
+           struct
+             include Arg
+
+             let find_invariant _ = Invariant.none
+           end
+           in
+           (module Arg: BiArgInvariant)
+         )
+         else (
+           let module Arg =
+           struct
+             module Node = ArgTool.Node
+             module Edge = MyARG.InlineEdge
+             let next _ = []
+             let prev _ = []
+             let find_invariant _ = Invariant.none
+             let main_entry =
+               let lvar = WitnessUtil.find_main_entry entrystates in
+               (fst lvar, snd lvar, -1)
+             let iter_nodes f = f main_entry
+             let query _ q = Queries.Result.top q
+           end
+           in
+           (module Arg: BiArgInvariant)
+         )
+      )
     in
 
     match spec with

From f8f89154b5d5fd9f2f80de3eae199540cd90fd52 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Sat, 28 Jun 2025 18:58:14 +0300
Subject: [PATCH 02/73] Consider InlinedEdges correctly in BFS for violation
 path construction

---
 src/arg/violation.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 4ae84a9fcf..6c514c9095 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -99,10 +99,10 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod
               match edge with
               | MyARG.CFGEdge _
               | InlineEntry _
-              | InlineReturn _ ->
+              | InlineReturn _
+              | InlinedEdge _ ->
                 if not (NHT.mem itered_nodes prev_node) then
                   NHT.replace next_nodes prev_node (edge, node)
-              | InlinedEdge _
               | ThreadEntry _ -> ()
             ) (Arg.prev node);
           bfs curs' (List.map snd (Arg.prev node) @ nexts)

From a16c8dea928ce2b8e59e630db9ee7c973076d382 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Sat, 28 Jun 2025 19:03:55 +0300
Subject: [PATCH 03/73] Add functionality to write violation yaml witnesses
 (with empty content)

---
 src/arg/violation.ml       | 21 ++++++++++++++++++++-
 src/witness/yamlWitness.ml |  7 +++++++
 2 files changed, 27 insertions(+), 1 deletion(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 6c514c9095..2e1349bba6 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -52,7 +52,26 @@ struct
     | Infeasible of (Node.t * MyARG.inline_edge * Node.t) list
     | Unknown
 
-  let check_path _ = Unknown
+  let write () =
+    (* TODO: duplicate code copied from YamlWitness.write *)
+    let input_files = GobConfig.get_string_list "files" in
+    let data_model = match GobConfig.get_string "exp.architecture" with
+      | "64bit" -> "LP64"
+      | "32bit" -> "ILP32"
+      | _ -> failwith "invalid architecture"
+    in
+    let specification = Option.map (fun (module Task: Svcomp.Task) ->
+        Svcomp.Specification.to_string Task.specification
+      ) !Svcomp.task
+    in
+    let task = YamlWitness.Entry.task ~input_files ~data_model ~specification in
+    let violation = [] in
+    let entry = YamlWitness.Entry.violation_sequence ~task ~violation in
+    let entries = [entry] in
+    let yaml_entries = List.rev_map YamlWitnessType.Entry.to_yaml entries in
+    YamlWitness.yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path"))
+
+  let check_path n = write (); Unknown
 end
 
 
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 9d04b597fa..3c031ee334 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -177,6 +177,13 @@ struct
       };
     metadata = metadata ~task ();
   }
+
+  let violation_sequence ~task ~(violation): Entry.t = {
+    entry_type = ViolationSequence {
+        content = violation;
+      };
+    metadata = metadata ~task ();
+  }
 end
 
 let yaml_entries_to_file yaml_entries file =

From 1756f675528e0b8fca86b148b513b4c808f661e8 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Sun, 29 Jun 2025 00:03:30 +0300
Subject: [PATCH 04/73] Create assumption "1" waypoints and a target waypoint
 from violation path's nodes

---
 src/arg/violation.ml       | 53 ++++++++++++++++++++++++++++++++++----
 src/witness/yamlWitness.ml | 24 +++++++++++++++++
 2 files changed, 72 insertions(+), 5 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 2e1349bba6..c913f6e62a 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -43,6 +43,8 @@ sig
   val check_path: (Node.t * MyARG.inline_edge * Node.t) list -> result
 end
 
+module CfgNode = Node
+
 module UnknownFeasibility (Node: MyARG.Node): Feasibility with module Node = Node =
 struct
   module Node = Node
@@ -52,7 +54,7 @@ struct
     | Infeasible of (Node.t * MyARG.inline_edge * Node.t) list
     | Unknown
 
-  let write () =
+  let write (path : (Node.t * MyARG.inline_edge * Node.t) list) =
     (* TODO: duplicate code copied from YamlWitness.write *)
     let input_files = GobConfig.get_string_list "files" in
     let data_model = match GobConfig.get_string "exp.architecture" with
@@ -65,13 +67,54 @@ struct
       ) !Svcomp.task
     in
     let task = YamlWitness.Entry.task ~input_files ~data_model ~specification in
-    let violation = [] in
-    let entry = YamlWitness.Entry.violation_sequence ~task ~violation in
-    let entries = [entry] in
+
+    let entries = [] in
+
+    let entries =
+      if YamlWitness.entry_type_enabled YamlWitnessType.ViolationSequence.entry_type then (
+
+        let loc prev =
+          let cfgNode = Node.cfgnode prev in
+          let location = CfgNode.location cfgNode in
+          let fundec = CfgNode.find_fundec cfgNode in
+          let location_function = fundec.svar.vname in
+          YamlWitness.Entry.location ~location ~location_function
+        in
+
+        let segments =
+          List.map (fun (prev, edge, node) ->
+              | _ ->
+                let constraint_ = YamlWitness.Entry.constraint_ ~value:(String "1") in
+                let assumption = YamlWitness.Entry.assumption ~location:(loc prev) ~constraint_ in
+                let waypoints = [YamlWitness.Entry.waypoint ~waypoint_type:(Assumption assumption)] in
+                YamlWitness.Entry.segment ~waypoints
+            ) path;
+        in
+
+        (* TODO: extremely inefficient *)
+        let target =
+          let (_,_,node) = BatList.last path in
+          let target = YamlWitness.Entry.violation_target ~location:(loc node) in
+          let waypoints = [YamlWitness.Entry.waypoint ~waypoint_type:(Target target)] in
+          YamlWitness.Entry.segment ~waypoints
+        in
+
+        let segments = List.append segments [target] in
+
+        let entry = YamlWitness.Entry.violation_sequence ~task ~violation:segments in
+        [entry]
+      )
+      else
+        entries
+    in  
+
     let yaml_entries = List.rev_map YamlWitnessType.Entry.to_yaml entries in
+    (* TODO: "witness generation summary" message *)
     YamlWitness.yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path"))
 
-  let check_path n = write (); Unknown
+  let check_path path =
+    write path;
+    Unknown
 end
 
 
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 3c031ee334..04d34a9d6c 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -178,6 +178,30 @@ struct
     metadata = metadata ~task ();
   }
 
+  let constraint_ ~value : ViolationSequence.Constraint.t = {
+    value = value;
+    format = Some "c_expression";
+  }
+
+  let assumption ~location ~constraint_ : ViolationSequence.Assumption.t = {
+    location = location;
+    action = "follow";
+    constraint_ = constraint_;
+  }
+
+  let violation_target ~location : ViolationSequence.Target.t = {
+    location = location;
+    action = "follow";
+  }
+
+  let waypoint ~waypoint_type : ViolationSequence.Waypoint.t = {
+    waypoint_type = waypoint_type;
+  }
+
+  let segment ~waypoints : ViolationSequence.Segment.t = {
+    segment = waypoints;
+  }
+
   let violation_sequence ~task ~(violation): Entry.t = {
     entry_type = ViolationSequence {
         content = violation;

From 03967351d7fe874fa01a2c319527fc441bda3030 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Sun, 29 Jun 2025 00:13:03 +0300
Subject: [PATCH 05/73] Differentiate function_enter, function_return and
 branching waypoints in violation witnesses

---
 src/arg/violation.ml       | 15 +++++++++++++++
 src/witness/yamlWitness.ml | 17 +++++++++++++++++
 2 files changed, 32 insertions(+)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index c913f6e62a..7693576eb4 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -83,6 +83,21 @@ struct
 
         let segments =
           List.map (fun (prev, edge, node) ->
+              match edge with
+              | MyARG.InlineEntry _ ->
+                let function_enter = YamlWitness.Entry.function_enter ~location:(loc prev) ~action:"follow" in
+                let waypoints = [YamlWitness.Entry.waypoint ~waypoint_type:(FunctionEnter function_enter)] in
+                YamlWitness.Entry.segment ~waypoints
+              | MyARG.InlineReturn _ ->
+                let constraint_ = YamlWitness.Entry.constraint_ ~value:(String "1") in
+                let function_return = YamlWitness.Entry.function_return ~location:(loc prev) ~action:"follow" ~constraint_ in
+                let waypoints = [YamlWitness.Entry.waypoint ~waypoint_type:(FunctionReturn function_return)] in
+                YamlWitness.Entry.segment ~waypoints
+              | MyARG.CFGEdge Test (_, bool) ->
+                let constraint_ = YamlWitness.Entry.constraint_ ~value:(String (Bool.to_string bool)) in
+                let branching = YamlWitness.Entry.branching ~location:(loc prev) ~action:"follow" ~constraint_ in
+                let waypoints = [YamlWitness.Entry.waypoint ~waypoint_type:(Branching branching)] in
+                YamlWitness.Entry.segment ~waypoints
               | _ ->
                 let constraint_ = YamlWitness.Entry.constraint_ ~value:(String "1") in
                 let assumption = YamlWitness.Entry.assumption ~location:(loc prev) ~constraint_ in
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 04d34a9d6c..164ddb4bb6 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -194,6 +194,23 @@ struct
     action = "follow";
   }
 
+  let function_enter ~location ~action : ViolationSequence.FunctionEnter.t = {
+    location = location;
+    action = action;
+  }
+
+  let function_return ~location ~action ~constraint_ : ViolationSequence.FunctionReturn.t = {
+    location = location;
+    action = action;
+    constraint_ = constraint_;
+  }
+
+  let branching ~location ~action ~constraint_ : ViolationSequence.Branching.t = {
+    location = location;
+    action = action;
+    constraint_ = constraint_;
+  }
+
   let waypoint ~waypoint_type : ViolationSequence.Waypoint.t = {
     waypoint_type = waypoint_type;
   }

From 87f5b8e76aea9c0e474eb78ec8d0006245797d49 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Sun, 29 Jun 2025 00:44:50 +0300
Subject: [PATCH 06/73] Use an efficient recursive function instead of map

---
 src/arg/violation.ml | 64 +++++++++++++++++++++++---------------------
 1 file changed, 33 insertions(+), 31 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 7693576eb4..2d0d5f1b75 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -55,6 +55,7 @@ struct
     | Unknown
 
   let write (path : (Node.t * MyARG.inline_edge * Node.t) list) =
+    let open YamlWitness.Entry in
     (* TODO: duplicate code copied from YamlWitness.write *)
     let input_files = GobConfig.get_string_list "files" in
     let data_model = match GobConfig.get_string "exp.architecture" with
@@ -66,7 +67,7 @@ struct
         Svcomp.Specification.to_string Task.specification
       ) !Svcomp.task
     in
-    let task = YamlWitness.Entry.task ~input_files ~data_model ~specification in
+    let task = task ~input_files ~data_model ~specification in
 
     let entries = [] in
 
@@ -81,40 +82,41 @@ struct
           YamlWitness.Entry.location ~location ~location_function
         in
 
-        let segments =
-          List.map (fun (prev, edge, node) ->
-              match edge with
-              | MyARG.InlineEntry _ ->
-                let function_enter = YamlWitness.Entry.function_enter ~location:(loc prev) ~action:"follow" in
-                let waypoints = [YamlWitness.Entry.waypoint ~waypoint_type:(FunctionEnter function_enter)] in
-                YamlWitness.Entry.segment ~waypoints
-              | MyARG.InlineReturn _ ->
-                let constraint_ = YamlWitness.Entry.constraint_ ~value:(String "1") in
-                let function_return = YamlWitness.Entry.function_return ~location:(loc prev) ~action:"follow" ~constraint_ in
-                let waypoints = [YamlWitness.Entry.waypoint ~waypoint_type:(FunctionReturn function_return)] in
-                YamlWitness.Entry.segment ~waypoints
-              | MyARG.CFGEdge Test (_, bool) ->
-                let constraint_ = YamlWitness.Entry.constraint_ ~value:(String (Bool.to_string bool)) in
-                let branching = YamlWitness.Entry.branching ~location:(loc prev) ~action:"follow" ~constraint_ in
-                let waypoints = [YamlWitness.Entry.waypoint ~waypoint_type:(Branching branching)] in
-                YamlWitness.Entry.segment ~waypoints
-              | _ ->
-                let constraint_ = YamlWitness.Entry.constraint_ ~value:(String "1") in
-                let assumption = YamlWitness.Entry.assumption ~location:(loc prev) ~constraint_ in
-                let waypoints = [YamlWitness.Entry.waypoint ~waypoint_type:(Assumption assumption)] in
-                YamlWitness.Entry.segment ~waypoints
-            ) path;
+        let segment_for_edge prev edge =
+          let location = loc prev in
+          match edge with
+          | MyARG.InlineEntry _ ->
+            let function_enter = function_enter ~location ~action:"follow" in
+            let waypoints = [waypoint ~waypoint_type:(FunctionEnter function_enter)] in
+            segment ~waypoints
+          | MyARG.InlineReturn _ ->
+            let constraint_ = constraint_ ~value:(String "1") in
+            let function_return = function_return ~location ~action:"follow" ~constraint_ in
+            let waypoints = [waypoint ~waypoint_type:(FunctionReturn function_return)] in
+            segment ~waypoints
+          | MyARG.CFGEdge Test (_, b) ->
+            let constraint_ = constraint_ ~value:(String (Bool.to_string b)) in
+            let branching = branching ~location ~action:"follow" ~constraint_ in
+            let waypoints = [waypoint ~waypoint_type:(Branching branching)] in
+            segment ~waypoints
+          | _ ->
+            let constraint_ = constraint_ ~value:(String "1") in
+            let assumption = assumption ~location ~constraint_ in
+            let waypoints = [waypoint ~waypoint_type:(Assumption assumption)] in
+            segment ~waypoints
         in
 
-        (* TODO: extremely inefficient *)
-        let target =
-          let (_,_,node) = BatList.last path in
-          let target = YamlWitness.Entry.violation_target ~location:(loc node) in
-          let waypoints = [YamlWitness.Entry.waypoint ~waypoint_type:(Target target)] in
-          YamlWitness.Entry.segment ~waypoints
+        let rec build_segments = function
+          | [] -> []
+          | [(prev, edge, node)] ->
+            let target = segment ~waypoints:[waypoint ~waypoint_type:(Target (violation_target ~location:(loc node)))] in
+            [segment_for_edge prev edge; target]
+          | (prev, edge, _) :: rest ->
+            let seg = segment_for_edge prev edge in
+            seg :: build_segments rest
         in
 
-        let segments = List.append segments [target] in
+        let segments = build_segments path in
 
         let entry = YamlWitness.Entry.violation_sequence ~task ~violation:segments in
         [entry]

From ae4679f9836dabe8de33a735af4f1e02809164a2 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 30 Jun 2025 00:17:11 +0300
Subject: [PATCH 07/73] Find the right locations using
 WitnessInvariant.location_location

---
 src/arg/violation.ml | 24 ++++++++++++++++++------
 1 file changed, 18 insertions(+), 6 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 2d0d5f1b75..2bb2740fb2 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -55,6 +55,13 @@ struct
     | Unknown
 
   let write (path : (Node.t * MyARG.inline_edge * Node.t) list) =
+    let module FileCfg =
+    struct
+      let file = !Cilfacade.current_file
+      module Cfg = (val !MyCFG.current_cfg)
+    end  in
+    let module WitnessInvariant = WitnessUtil.YamlInvariant (FileCfg) in
+
     let open YamlWitness.Entry in
     (* TODO: duplicate code copied from YamlWitness.write *)
     let input_files = GobConfig.get_string_list "files" in
@@ -73,17 +80,18 @@ struct
 
     let entries =
       if YamlWitness.entry_type_enabled YamlWitnessType.ViolationSequence.entry_type then (
+        let open GobOption.Syntax in
 
         let loc prev =
           let cfgNode = Node.cfgnode prev in
-          let location = CfgNode.location cfgNode in
+          let+ location = WitnessInvariant.location_location cfgNode in
           let fundec = CfgNode.find_fundec cfgNode in
           let location_function = fundec.svar.vname in
           YamlWitness.Entry.location ~location ~location_function
         in
 
         let segment_for_edge prev edge =
-          let location = loc prev in
+          let+ location = loc prev in
           match edge with
           | MyARG.InlineEntry _ ->
             let function_enter = function_enter ~location ~action:"follow" in
@@ -109,11 +117,15 @@ struct
         let rec build_segments = function
           | [] -> []
           | [(prev, edge, node)] ->
-            let target = segment ~waypoints:[waypoint ~waypoint_type:(Target (violation_target ~location:(loc node)))] in
-            [segment_for_edge prev edge; target]
+            let target = segment ~waypoints:[waypoint ~waypoint_type:(Target (violation_target ~location:(Option.get (loc node))))] in
+            begin match segment_for_edge prev edge with
+              | Some seg -> [seg; target]
+              | None -> [target]
+            end
           | (prev, edge, _) :: rest ->
-            let seg = segment_for_edge prev edge in
-            seg :: build_segments rest
+            match segment_for_edge prev edge with
+            | Some seg -> seg :: build_segments rest
+            | None -> build_segments rest
         in
 
         let segments = build_segments path in

From 1516a74ef0eff371b210a981957fd61d62a5a9e9 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 30 Jun 2025 00:24:32 +0300
Subject: [PATCH 08/73] Disable function entry/return waypoints for now due to
 missing correct locations

---
 src/arg/violation.ml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 2bb2740fb2..0735d4df8b 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -93,6 +93,11 @@ struct
         let segment_for_edge prev edge =
           let+ location = loc prev in
           match edge with
+          (* TODO: Correct locations for function entry and return are currently unavailable.
+             As specified by the Witness 2.0 format, these locations must point to
+             the closing parenthesis after the function's parameter list.
+          *)
+          (*
           | MyARG.InlineEntry _ ->
             let function_enter = function_enter ~location ~action:"follow" in
             let waypoints = [waypoint ~waypoint_type:(FunctionEnter function_enter)] in
@@ -102,6 +107,7 @@ struct
             let function_return = function_return ~location ~action:"follow" ~constraint_ in
             let waypoints = [waypoint ~waypoint_type:(FunctionReturn function_return)] in
             segment ~waypoints
+          *)
           | MyARG.CFGEdge Test (_, b) ->
             let constraint_ = constraint_ ~value:(String (Bool.to_string b)) in
             let branching = branching ~location ~action:"follow" ~constraint_ in

From a3fd139ac892b26ab330e2a745bde8b9bee1fbef Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 1 Jul 2025 09:33:03 +0300
Subject: [PATCH 09/73] Change violation path finding direction from bottom-up
 to top-down

due to the uncil-ing only changing next but not the prev nodes
---
 src/arg/violation.ml | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 0735d4df8b..83a0545d3e 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -153,8 +153,6 @@ struct
 end
 
 
-exception Found
-
 module type PathArg = MyARG.S with module Edge = MyARG.InlineEdge
 
 type 'node result =
@@ -182,27 +180,29 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod
       ) path
   in
 
+  let exception Found of Arg.Node.t in
+
   let find_path nodes =
     let next_nodes = NHT.create 100 in
 
     let itered_nodes = NHT.create 100 in
     let rec bfs curs nexts = match curs with
       | node :: curs' ->
-        if Arg.Node.equal node Arg.main_entry then
-          raise Found
+        if BatList.mem_cmp Arg.Node.compare node Arg.violations then
+          raise (Found node)
         else if not (NHT.mem itered_nodes node) then begin
           NHT.replace itered_nodes node ();
-          List.iter (fun (edge, prev_node) ->
+          List.iter (fun (edge, next_node) ->
               match edge with
               | MyARG.CFGEdge _
               | InlineEntry _
               | InlineReturn _
               | InlinedEdge _ ->
-                if not (NHT.mem itered_nodes prev_node) then
-                  NHT.replace next_nodes prev_node (edge, node)
+                if not (NHT.mem itered_nodes next_node) then
+                  NHT.replace next_nodes next_node (edge, node)
               | ThreadEntry _ -> ()
-            ) (Arg.prev node);
-          bfs curs' (List.map snd (Arg.prev node) @ nexts)
+            ) (Arg.next node);
+          bfs curs' (List.map snd (Arg.next node) @ nexts)
         end
         else
           bfs curs' nexts
@@ -213,11 +213,11 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod
     in
 
     try bfs nodes []; None with
-    | Found ->
-      Some (trace_path next_nodes Arg.main_entry)
+    | Found violation ->
+      Some (List.rev_map (fun (n1, e, n2) -> (n2, e, n1)) (trace_path next_nodes violation)) (* TODO: inefficient rev *)
   in
 
-  begin match find_path Arg.violations with
+  begin match find_path [Arg.main_entry] with
     | Some path ->
       print_path path;
       begin match Feasibility.check_path path with

From a0ff4faa1619dadace7b00b5e6035b4f7586b6b1 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Wed, 2 Jul 2025 11:26:30 +0300
Subject: [PATCH 10/73] Add "mapping_start failed" to Yaml.to_string error
 handling

---
 src/util/std/gobYaml.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/util/std/gobYaml.ml b/src/util/std/gobYaml.ml
index 4c8576ade2..e1473d32d4 100644
--- a/src/util/std/gobYaml.ml
+++ b/src/util/std/gobYaml.ml
@@ -3,7 +3,7 @@ let to_string' ?(len=65535 * 4) ?encoding ?scalar_style ?layout_style v =
   let rec aux len =
     match Yaml.to_string ~len ?encoding ?scalar_style ?layout_style v with
     | Ok _ as o -> o
-    | Error (`Msg ("scalar failed" | "doc_end failed" | "seq_end failed")) when len < Sys.max_string_length / 2 ->
+    | Error (`Msg ("scalar failed" | "doc_end failed" | "seq_end failed" | "mapping_start failed")) when len < Sys.max_string_length / 2 ->
       aux (len * 2)
     | Error (`Msg _) as e -> e
   in

From d9cb04b1cc84d175390b03b87831689e91f243f6 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Wed, 2 Jul 2025 11:33:00 +0300
Subject: [PATCH 11/73] Temporarily disable conf immutability to bypass
 restriction on adding analyses

---
 src/config/gobConfig.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/config/gobConfig.ml b/src/config/gobConfig.ml
index 1a3daf616d..7ba183c43b 100644
--- a/src/config/gobConfig.ml
+++ b/src/config/gobConfig.ml
@@ -351,7 +351,10 @@ struct
   (** Sets a value, preventing changes when the configuration is immutable and invalidating the cache.
       @raise Immutable *)
   let set_value v o pth =
-    if is_immutable () then raise (Immutable pth);
+    (* TODO: only needed for adding the observers:
+       rewrite so that there is only one observer-analysis
+       that handles all observes internally without new analyses being added. *)
+    (* if is_immutable () then raise (Immutable pth); *)
     drop_memo ();
     unsafe_set_value v o pth
 

From 745a4e8724198dd0dd87569ff391916d65d08d4d Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Wed, 2 Jul 2025 11:35:49 +0300
Subject: [PATCH 12/73] Make `spec_module` a `ResettableLazy` to enable
 resetting hashcons lifters

---
 src/framework/control.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/framework/control.ml b/src/framework/control.ml
index e990810d44..e64439e9d8 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -16,7 +16,7 @@ open SpecLifters
 module type S2S = Spec2Spec
 
 (* spec is lazy, so HConsed table in Hashcons lifters is preserved between analyses in server mode *)
-let spec_module: (module Spec) Lazy.t = lazy (
+let spec_module: (module Spec) ResettableLazy.t = ResettableLazy.from_fun (fun () ->
   GobConfig.building_spec := true;
   let arg_enabled = get_bool "exp.arg.enabled" in
   let termination_enabled = List.mem "termination" (get_string_list "ana.activated") in (* check if loop termination analysis is enabled*)
@@ -50,12 +50,12 @@ let spec_module: (module Spec) Lazy.t = lazy (
   in
   GobConfig.building_spec := false;
   ControlSpecC.control_spec_c := (module S1.C);
-  (module S1)
+  (module S1 : Spec)
 )
 
 (** gets Spec for current options *)
 let get_spec (): (module Spec) =
-  Lazy.force spec_module
+  ResettableLazy.force spec_module
 
 let current_node_state_json : (Node.t -> Yojson.Safe.t option) ref = ref (fun _ -> None)
 
@@ -849,6 +849,7 @@ let rec analyze_loop (module CFG : CfgBidirSkip) file fs change_info =
         Whoever raised the exception should've modified some global state
         to do a more precise analysis next time. *)
     (* TODO: do some more incremental refinement and reuse parts of solution *)
+    ResettableLazy.reset spec_module;
     analyze_loop (module CFG) file fs change_info
 
 (** The main function to perform the selected analyses. *)

From 0c1cea35fff568fd6005dfd5f5647e99e1d0dd6b Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Wed, 2 Jul 2025 12:41:44 +0300
Subject: [PATCH 13/73] Add functionality to use witch for result refinement

---
 src/arg/violation.ml           | 38 +++++++++++++++++++++++++++++++++-
 src/config/options.schema.json |  6 ++++++
 2 files changed, 43 insertions(+), 1 deletion(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 83a0545d3e..de0c2fa305 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -147,9 +147,45 @@ struct
     (* TODO: "witness generation summary" message *)
     YamlWitness.yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path"))
 
+  let read_command_output command =
+    let (ic, _) as process = Unix.open_process command in
+    let rec read_lines acc =
+      try
+        let line = input_line ic in
+        read_lines (line :: acc)
+      with End_of_file ->
+        ignore (Unix.close_process process);
+        acc
+    in
+    read_lines []
+
+  let extract_result_line lines =
+    let re = Str.regexp "^RESULT: \\(.*\\)$" in
+    List.find_map (fun line -> if Str.string_match re line 0 then Some (Str.matched_group 1 line) else None) lines
+
+  let check_feasability_with_witch witch path =
+    let files = String.concat " " (GobConfig.get_string_list "files") in
+    let data_model = match GobConfig.get_string "exp.architecture" with
+      | "64bit" -> "--64"
+      | "32bit" -> "--32"
+      | _ -> failwith "invalid architecture"
+    in
+    let witness_file_path = GobConfig.get_string "witness.yaml.path" in
+    (*  ../witch/scripts/symbiotic --witness-check ../analyzer/witness.yml --32 ../analyzer/violation-witness.c *)
+    let command = Printf.sprintf "%s --witness-check %s %s %s" witch witness_file_path data_model files in
+    let lines = read_command_output command in
+    match extract_result_line lines with
+    | Some "true" -> Printf.printf "Verification result: false\n"; Infeasible path
+    | Some "false" -> Printf.printf "Verification result: true\n"; Feasible
+    | Some _ -> Unknown
+    | None -> Unknown
+
   let check_path path =
     write path;
-    Unknown
+    let witch = GobConfig.get_string "exp.witch" in
+    match witch with
+    | "" -> Unknown
+    | _ -> check_feasability_with_witch witch path
 end
 
 
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index ae26553ec0..4c96800862 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -2059,6 +2059,12 @@
             }
           },
           "additionalProperties": false
+        },
+        "witch": {
+          "title": "exp.witch",
+          "description": "Path to the Witch executable for result refinement.",
+          "type": "string",
+          "default": ""
         }
       },
       "additionalProperties": false

From f73b8fa1473cd52023a3567c083226711b0e9619 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Wed, 2 Jul 2025 14:40:19 +0300
Subject: [PATCH 14/73] Take into account that the verdicts can have suffixes
 (e.g. false(unreach-call))

---
 src/arg/violation.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index de0c2fa305..0b8bfc201b 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -175,8 +175,8 @@ struct
     let command = Printf.sprintf "%s --witness-check %s %s %s" witch witness_file_path data_model files in
     let lines = read_command_output command in
     match extract_result_line lines with
-    | Some "true" -> Printf.printf "Verification result: false\n"; Infeasible path
-    | Some "false" -> Printf.printf "Verification result: true\n"; Feasible
+    | Some result when String.starts_with ~prefix:"true" result -> Printf.printf "Verification result: %s\n" result; Infeasible path
+    | Some result when String.starts_with ~prefix:"false" result -> Printf.printf "Verification result: %s\n" result; Feasible
     | Some _ -> Unknown
     | None -> Unknown
 

From c9eb38ec050602ce8ee9446cee730a8e629de40b Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 3 Jul 2025 12:28:57 +0300
Subject: [PATCH 15/73] Bugfix: correctly account for InlinedEdges

---
 src/arg/violation.ml | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 0b8bfc201b..06614c1b86 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -228,17 +228,19 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod
           raise (Found node)
         else if not (NHT.mem itered_nodes node) then begin
           NHT.replace itered_nodes node ();
-          List.iter (fun (edge, next_node) ->
+          let next_nodes = List.filter_map (fun (edge, next_node) ->
               match edge with
               | MyARG.CFGEdge _
               | InlineEntry _
-              | InlineReturn _
-              | InlinedEdge _ ->
+              | InlineReturn _ ->
                 if not (NHT.mem itered_nodes next_node) then
-                  NHT.replace next_nodes next_node (edge, node)
-              | ThreadEntry _ -> ()
-            ) (Arg.next node);
-          bfs curs' (List.map snd (Arg.next node) @ nexts)
+                  NHT.replace next_nodes next_node (edge, node);
+                Some next_node
+              | InlinedEdge _
+              | ThreadEntry _ -> None
+            ) (Arg.next node)
+          in
+          bfs curs' (next_nodes @ nexts)
         end
         else
           bfs curs' nexts

From f40198a87fc64e676bbcb2513d499f577b6f259a Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Fri, 4 Jul 2025 12:38:29 +0300
Subject: [PATCH 16/73] Do not create waypoints of return edges (due to void
 fun-s not having return locations)

---
 src/arg/violation.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 06614c1b86..5b2c433a19 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -91,7 +91,6 @@ struct
         in
 
         let segment_for_edge prev edge =
-          let+ location = loc prev in
           match edge with
           (* TODO: Correct locations for function entry and return are currently unavailable.
              As specified by the Witness 2.0 format, these locations must point to
@@ -108,12 +107,15 @@ struct
             let waypoints = [waypoint ~waypoint_type:(FunctionReturn function_return)] in
             segment ~waypoints
           *)
+          | MyARG.CFGEdge Ret (None, _) -> None
           | MyARG.CFGEdge Test (_, b) ->
+            let+ location = loc prev in
             let constraint_ = constraint_ ~value:(String (Bool.to_string b)) in
             let branching = branching ~location ~action:"follow" ~constraint_ in
             let waypoints = [waypoint ~waypoint_type:(Branching branching)] in
             segment ~waypoints
           | _ ->
+            let+ location = loc prev in
             let constraint_ = constraint_ ~value:(String "1") in
             let assumption = assumption ~location ~constraint_ in
             let waypoints = [waypoint ~waypoint_type:(Assumption assumption)] in

From 29efcdeca2c357f46517df805032a50824d5165c Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Fri, 4 Jul 2025 12:42:38 +0300
Subject: [PATCH 17/73] Do uncilling only for witness waypoints (to keep the
 cilled path as automaton for reanalysis)

---
 src/arg/argTools.ml    |  2 +-
 src/arg/violation.ml   | 54 ++++++++++++++++++++++++++++++++----------
 src/witness/witness.ml |  2 +-
 3 files changed, 43 insertions(+), 15 deletions(-)

diff --git a/src/arg/argTools.ml b/src/arg/argTools.ml
index a220120912..1abc009ab0 100644
--- a/src/arg/argTools.ml
+++ b/src/arg/argTools.ml
@@ -214,7 +214,7 @@ struct
     let module Arg =
     struct
       open MyARG
-      module ArgIntra = UnCilTernaryIntra (UnCilLogicIntra (CfgIntra (FileCfg.Cfg)))
+      module ArgIntra = CfgIntra (FileCfg.Cfg) (* TODO: put UnCilTernaryIntra and UnCilLogicIntra back so that the uncil option works *)
       include Intra (ArgIntra) (Arg)
 
       let prev = witness_prev
diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 5b2c433a19..031620363f 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -1,4 +1,5 @@
 (** Violation checking in an ARG. *)
+open MyARG
 
 module type ViolationArg =
 sig
@@ -45,9 +46,10 @@ end
 
 module CfgNode = Node
 
-module UnknownFeasibility (Node: MyARG.Node): Feasibility with module Node = Node =
+module UnknownFeasibility (Arg: ArgTools.BiArg): Feasibility with module Node = Arg.Node =
 struct
-  module Node = Node
+  module Node = Arg.Node
+  module SegMap = Map.Make (Node)
 
   type result =
     | Feasible
@@ -59,8 +61,9 @@ struct
     struct
       let file = !Cilfacade.current_file
       module Cfg = (val !MyCFG.current_cfg)
-    end  in
+    end in
     let module WitnessInvariant = WitnessUtil.YamlInvariant (FileCfg) in
+    let module UnCilArg = Intra (UnCilTernaryIntra (UnCilLogicIntra (CfgIntra (FileCfg.Cfg)))) (Arg) in
 
     let open YamlWitness.Entry in
     (* TODO: duplicate code copied from YamlWitness.write *)
@@ -122,21 +125,46 @@ struct
             segment ~waypoints
         in
 
-        let rec build_segments = function
-          | [] -> []
+        let find_next_segment prev edge node segmap =
+          let nexts = UnCilArg.next prev in
+          let potential_nodes = List.filter_map (fun (new_edge, new_node) ->
+              match new_edge with
+              | MyARG.InlinedEdge _ -> None
+              | _ ->
+                let+ res : YamlWitnessType.ViolationSequence.Segment.t list = SegMap.find_opt new_node segmap in
+                (new_edge, res)
+            ) nexts in
+          assert (List.length potential_nodes == 1); (* TODO: there might be more than one node *)
+          List.hd potential_nodes
+        in
+
+        let rec build_segments path =
+          match path with
+          | [] -> SegMap.empty
           | [(prev, edge, node)] ->
             let target = segment ~waypoints:[waypoint ~waypoint_type:(Target (violation_target ~location:(Option.get (loc node))))] in
-            begin match segment_for_edge prev edge with
-              | Some seg -> [seg; target]
+            let new_seg = match segment_for_edge prev edge with
+              | Some seg -> seg :: [target]
               | None -> [target]
-            end
-          | (prev, edge, _) :: rest ->
-            match segment_for_edge prev edge with
-            | Some seg -> seg :: build_segments rest
-            | None -> build_segments rest
+            in
+            let segmap = SegMap.singleton node [target] in
+            SegMap.add prev new_seg segmap
+          | (prev, edge, node) :: rest ->
+            let segmap = build_segments rest in
+            let new_edge, uncilled = find_next_segment prev edge node segmap in
+            let this_seg = match segment_for_edge prev new_edge with
+              | Some seg -> seg :: uncilled
+              | None -> uncilled
+            in
+            SegMap.add prev this_seg segmap
         in
 
-        let segments = build_segments path in
+        let segmap = build_segments path in
+        let segments =
+          match path with
+          | [] -> []
+          | (prev, _, _) :: _ -> SegMap.find prev segmap
+        in
 
         let entry = YamlWitness.Entry.violation_sequence ~task ~violation:segments in
         [entry]
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index bd3123b6f4..88d71fa4ed 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -166,7 +166,7 @@ struct
           Result.Unknown
         in
         if get_bool "ana.wp" then (
-          match Violation.find_path (module ViolationArg) (module ViolationZ3.WP (ViolationArg.Node)) with
+          match Violation.find_path (module ViolationArg) (module ViolationZ3.WP (ViolationArg)) with
           | Feasible (module PathArg) ->
             (* TODO: add assumptions *)
             Result.False (Some spec)

From a35192dc6f6337b7bbd6e88ba0a81383fd0f8252 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Fri, 4 Jul 2025 12:45:36 +0300
Subject: [PATCH 18/73] Add `--guide-only` flag for witch

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

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 031620363f..e2fb48ea58 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -202,7 +202,7 @@ struct
     in
     let witness_file_path = GobConfig.get_string "witness.yaml.path" in
     (*  ../witch/scripts/symbiotic --witness-check ../analyzer/witness.yml --32 ../analyzer/violation-witness.c *)
-    let command = Printf.sprintf "%s --witness-check %s %s %s" witch witness_file_path data_model files in
+    let command = Printf.sprintf "%s --witness-check %s %s --guide-only %s" witch witness_file_path data_model files in
     let lines = read_command_output command in
     match extract_result_line lines with
     | Some result when String.starts_with ~prefix:"true" result -> Printf.printf "Verification result: %s\n" result; Infeasible path

From 08a42eb22dadab7b3a8f250ee11b7a061e60b9fc Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Fri, 4 Jul 2025 21:47:11 +0300
Subject: [PATCH 19/73] Trim path prefix up to the corresponding waypoint
 preceding the first unreachable segment reported by Witch

---
 src/arg/violation.ml | 80 +++++++++++++++++++++++++++++++-------------
 1 file changed, 57 insertions(+), 23 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index e2fb48ea58..1ef321099b 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -50,6 +50,7 @@ module UnknownFeasibility (Arg: ArgTools.BiArg): Feasibility with module Node =
 struct
   module Node = Arg.Node
   module SegMap = Map.Make (Node)
+  module SegNrToPathMap = Map.Make (Int)
 
   type result =
     | Feasible
@@ -81,7 +82,7 @@ struct
 
     let entries = [] in
 
-    let entries =
+    let entries, segToPathMap, segments =
       if YamlWitness.entry_type_enabled YamlWitnessType.ViolationSequence.entry_type then (
         let open GobOption.Syntax in
 
@@ -138,28 +139,32 @@ struct
           List.hd potential_nodes
         in
 
-        let rec build_segments path =
+        let rec build_segments path segToPathMap segNr =
           match path with
-          | [] -> SegMap.empty
-          | [(prev, edge, node)] ->
+          | [] -> SegMap.empty, segToPathMap, 0
+          | [(prev, edge, node)] as sub_path ->
             let target = segment ~waypoints:[waypoint ~waypoint_type:(Target (violation_target ~location:(Option.get (loc node))))] in
-            let new_seg = match segment_for_edge prev edge with
-              | Some seg -> seg :: [target]
-              | None -> [target]
+            let this_seg, segToPathMap, segNr = match segment_for_edge prev edge with
+              | Some seg ->
+                let segToPathMap1 = SegNrToPathMap.add 0 sub_path segToPathMap in
+                let segToPathMap2 = SegNrToPathMap.add 1 sub_path segToPathMap1 in
+                seg :: [target], segToPathMap2, 2
+              | None ->
+                [target], SegNrToPathMap.add 0 sub_path segToPathMap, 1
             in
             let segmap = SegMap.singleton node [target] in
-            SegMap.add prev new_seg segmap
-          | (prev, edge, node) :: rest ->
-            let segmap = build_segments rest in
+            SegMap.add prev this_seg segmap, segToPathMap, segNr
+          | (prev, edge, node) :: rest as sub_path ->
+            let segmap, segToPathMap, segNr = build_segments rest segToPathMap segNr in
             let new_edge, uncilled = find_next_segment prev edge node segmap in
-            let this_seg = match segment_for_edge prev new_edge with
-              | Some seg -> seg :: uncilled
-              | None -> uncilled
+            let this_seg, segToPathMap, segNr = match segment_for_edge prev new_edge with
+              | Some seg -> seg :: uncilled, SegNrToPathMap.add segNr sub_path segToPathMap, segNr + 1
+              | None -> uncilled, segToPathMap, segNr
             in
-            SegMap.add prev this_seg segmap
+            SegMap.add prev this_seg segmap, segToPathMap, segNr
         in
 
-        let segmap = build_segments path in
+        let segmap, segToPathMap, _ = build_segments path SegNrToPathMap.empty 0 in
         let segments =
           match path with
           | [] -> []
@@ -167,15 +172,16 @@ struct
         in
 
         let entry = YamlWitness.Entry.violation_sequence ~task ~violation:segments in
-        [entry]
+        [entry], segToPathMap, segments
       )
       else
-        entries
-    in  
+        entries, SegNrToPathMap.empty, []
+    in
 
     let yaml_entries = List.rev_map YamlWitnessType.Entry.to_yaml entries in
     (* TODO: "witness generation summary" message *)
-    YamlWitness.yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path"))
+    YamlWitness.yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path"));
+    segToPathMap, segments
 
   let read_command_output command =
     let (ic, _) as process = Unix.open_process command in
@@ -193,7 +199,15 @@ struct
     let re = Str.regexp "^RESULT: \\(.*\\)$" in
     List.find_map (fun line -> if Str.string_match re line 0 then Some (Str.matched_group 1 line) else None) lines
 
-  let check_feasability_with_witch witch path =
+  (* TODO: find both (result and seg nr) with one traversal *)
+  let extract_unreach_seg_nr lines =
+    let re = Str.regexp "segment \\([0-9]+\\) cannot be passed" in
+    List.find_map (fun line ->
+        try ignore (Str.search_forward re line 0); Some (int_of_string (Str.matched_group 1 line))
+        with Not_found -> None
+      ) lines
+
+  let run_witch witch =
     let files = String.concat " " (GobConfig.get_string_list "files") in
     let data_model = match GobConfig.get_string "exp.architecture" with
       | "64bit" -> "--64"
@@ -203,7 +217,24 @@ struct
     let witness_file_path = GobConfig.get_string "witness.yaml.path" in
     (*  ../witch/scripts/symbiotic --witness-check ../analyzer/witness.yml --32 ../analyzer/violation-witness.c *)
     let command = Printf.sprintf "%s --witness-check %s %s --guide-only %s" witch witness_file_path data_model files in
-    let lines = read_command_output command in
+    read_command_output command
+
+  let get_unreachable_path lines (path: (Node.t * inline_edge * Node.t) list) (segToPathMap, segments) =
+    let has_no_branching_before_unreachable segments seg_nr =
+      let rec check i: YamlWitnessType.ViolationSequence.Segment.t list -> bool = function
+        | _ when i == seg_nr -> true
+        | [] -> true
+        | {segment = {waypoint_type = Branching _} :: _} :: _ -> false
+        | _ :: rest -> check (i + 1) rest
+      in
+      check 0 segments
+    in 
+
+    match extract_unreach_seg_nr lines with
+    | Some seg_nr when has_no_branching_before_unreachable segments seg_nr -> SegNrToPathMap.find (List.length segments - seg_nr -1) segToPathMap
+    | _ -> path
+
+  let check_feasability_with_witch lines path =
     match extract_result_line lines with
     | Some result when String.starts_with ~prefix:"true" result -> Printf.printf "Verification result: %s\n" result; Infeasible path
     | Some result when String.starts_with ~prefix:"false" result -> Printf.printf "Verification result: %s\n" result; Feasible
@@ -211,11 +242,14 @@ struct
     | None -> Unknown
 
   let check_path path =
-    write path;
+    let seg = write path in
     let witch = GobConfig.get_string "exp.witch" in
     match witch with
     | "" -> Unknown
-    | _ -> check_feasability_with_witch witch path
+    | _ ->
+      let lines = run_witch witch in
+      let path = get_unreachable_path lines path seg in
+      check_feasability_with_witch lines path
 end
 
 

From 0d90cf9e2db563150b07b5062ce44f2d5f860e47 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Sun, 6 Jul 2025 23:21:24 +0300
Subject: [PATCH 20/73] Do not cut paths that contain the unreachable node
 within a loop

---
 src/arg/violation.ml | 57 ++++++++++++++++++++++++++++++++++----------
 1 file changed, 44 insertions(+), 13 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 1ef321099b..79636d6a9f 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -41,7 +41,7 @@ sig
     | Infeasible of (Node.t * MyARG.inline_edge * Node.t) list
     | Unknown
 
-  val check_path: (Node.t * MyARG.inline_edge * Node.t) list -> result
+  val check_path: (Node.t * MyARG.inline_edge * Node.t) list -> (Node.t, Node.t list) Hashtbl.t -> result
 end
 
 module CfgNode = Node
@@ -219,7 +219,7 @@ struct
     let command = Printf.sprintf "%s --witness-check %s %s --guide-only %s" witch witness_file_path data_model files in
     read_command_output command
 
-  let get_unreachable_path lines (path: (Node.t * inline_edge * Node.t) list) (segToPathMap, segments) =
+  let get_unreachable_path lines (path: (Node.t * inline_edge * Node.t) list) (segToPathMap, segments) node_to_stack =
     let has_no_branching_before_unreachable segments seg_nr =
       let rec check i: YamlWitnessType.ViolationSequence.Segment.t list -> bool = function
         | _ when i == seg_nr -> true
@@ -228,10 +228,27 @@ struct
         | _ :: rest -> check (i + 1) rest
       in
       check 0 segments
-    in 
+    in
+
+    let is_within_loop (node, _, _) =
+      let callstack = List.rev (Hashtbl.find node_to_stack node) in (* TODO: inefficient rev *)
+      let cfg_node = match callstack with
+        | hd :: _ -> Node.cfgnode hd
+        | [] -> Node.cfgnode node
+      in
+      Logs.error "node: %a" CfgNode.pretty cfg_node;
+      let scc_components = CfgTools.node_scc_global in
+      match CfgTools.NH.find_option scc_components cfg_node with
+      | Some scc when CfgTools.NH.length scc.nodes > 1 -> true
+      | _ -> false
+    in
 
     match extract_unreach_seg_nr lines with
-    | Some seg_nr when has_no_branching_before_unreachable segments seg_nr -> SegNrToPathMap.find (List.length segments - seg_nr -1) segToPathMap
+    | Some seg_nr when has_no_branching_before_unreachable segments seg_nr ->
+      (* TODO: consider seg_nr == 0 separately *)
+      let path_suffix = SegNrToPathMap.find (List.length segments - seg_nr -1) segToPathMap in
+      if not (is_within_loop (List.hd path_suffix)) then path_suffix
+      else path
     | _ -> path
 
   let check_feasability_with_witch lines path =
@@ -241,14 +258,14 @@ struct
     | Some _ -> Unknown
     | None -> Unknown
 
-  let check_path path =
+  let check_path path node_to_stack =
     let seg = write path in
     let witch = GobConfig.get_string "exp.witch" in
     match witch with
     | "" -> Unknown
     | _ ->
       let lines = run_witch witch in
-      let path = get_unreachable_path lines path seg in
+      let path = get_unreachable_path lines path seg node_to_stack in
       check_feasability_with_witch lines path
 end
 
@@ -284,8 +301,20 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod
 
   let find_path nodes =
     let next_nodes = NHT.create 100 in
-
     let itered_nodes = NHT.create 100 in
+    let node_to_stack = Hashtbl.create 100 in
+
+    let collect_callstack node edge next_node =
+      let prev_stack = Hashtbl.find_opt node_to_stack node |> Option.value ~default:[] in
+      let new_stack = match edge with
+        | MyARG.CFGEdge (Entry f) when f.svar.vname <> "main" -> node :: prev_stack
+        | InlineEntry _ -> node :: prev_stack
+        | InlineReturn _ -> BatList.drop 1 prev_stack
+        | _ -> prev_stack
+      in
+      Hashtbl.replace node_to_stack next_node new_stack;
+    in
+
     let rec bfs curs nexts = match curs with
       | node :: curs' ->
         if BatList.mem_cmp Arg.Node.compare node Arg.violations then
@@ -297,8 +326,10 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod
               | MyARG.CFGEdge _
               | InlineEntry _
               | InlineReturn _ ->
-                if not (NHT.mem itered_nodes next_node) then
+                if not (NHT.mem itered_nodes next_node) then (
                   NHT.replace next_nodes next_node (edge, node);
+                  collect_callstack node edge next_node
+                );
                 Some next_node
               | InlinedEdge _
               | ThreadEntry _ -> None
@@ -316,13 +347,13 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod
 
     try bfs nodes []; None with
     | Found violation ->
-      Some (List.rev_map (fun (n1, e, n2) -> (n2, e, n1)) (trace_path next_nodes violation)) (* TODO: inefficient rev *)
-  in
+      Some ((List.rev_map (fun (n1, e, n2) -> (n2, e, n1)) (trace_path next_nodes violation)), node_to_stack) (* TODO: inefficient rev *)
+    in
 
-  begin match find_path [Arg.main_entry] with
-    | Some path ->
+    begin match find_path [Arg.main_entry] with
+    | Some (path, node_to_stack) ->
       print_path path;
-      begin match Feasibility.check_path path with
+      begin match Feasibility.check_path path node_to_stack with
         | Feasibility.Feasible ->
           Logs.debug "feasible";
 

From da5b5940630cb6ca4e31b215e3e0126b304c40de Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Sun, 6 Jul 2025 23:21:35 +0300
Subject: [PATCH 21/73] Log all of Witch'es output

---
 src/arg/violation.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 79636d6a9f..28ded0818c 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -188,6 +188,7 @@ struct
     let rec read_lines acc =
       try
         let line = input_line ic in
+        Logs.info "Witch: %s" line;
         read_lines (line :: acc)
       with End_of_file ->
         ignore (Unix.close_process process);

From 6cc99b7432971b114c92349e1c221b0d06ca15c0 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Sun, 6 Jul 2025 23:27:55 +0300
Subject: [PATCH 22/73] Remove forgotten logging for debugging

---
 src/arg/violation.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 28ded0818c..73694685ba 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -237,7 +237,6 @@ struct
         | hd :: _ -> Node.cfgnode hd
         | [] -> Node.cfgnode node
       in
-      Logs.error "node: %a" CfgNode.pretty cfg_node;
       let scc_components = CfgTools.node_scc_global in
       match CfgTools.NH.find_option scc_components cfg_node with
       | Some scc when CfgTools.NH.length scc.nodes > 1 -> true

From b47805c82370266af44ae152affe3f8585f00230 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 7 Jul 2025 12:15:27 +0300
Subject: [PATCH 23/73] Do not trim path when it includes setjump calls

---
 src/arg/violation.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 73694685ba..4d806b4642 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -243,11 +243,20 @@ struct
       | _ -> false
     in
 
+    let has_setjump_calls (path: (Node.t * inline_edge * Node.t) list): bool =
+      let rec check: (Node.t * inline_edge * Node.t) list -> bool = function
+        | [] -> false
+        | (_, MyARG.CFGEdge Proc (_, Lval((Var v, _)), _) , _) :: _ when v.vname = "_setjmp" -> true
+        | _ :: rest -> check rest
+      in
+      check path
+    in
+
     match extract_unreach_seg_nr lines with
     | Some seg_nr when has_no_branching_before_unreachable segments seg_nr ->
       (* TODO: consider seg_nr == 0 separately *)
       let path_suffix = SegNrToPathMap.find (List.length segments - seg_nr -1) segToPathMap in
-      if not (is_within_loop (List.hd path_suffix)) then path_suffix
+      if not (is_within_loop (List.hd path_suffix)) && not (has_setjump_calls path) then path_suffix
       else path
     | _ -> path
 

From 84bf053aab840c11d848d54d24b578510bd2eadb Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 7 Jul 2025 12:47:06 +0300
Subject: [PATCH 24/73] Replace all `==` with `=`

---
 src/arg/violation.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 4d806b4642..5a8016b3ec 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -135,7 +135,7 @@ struct
                 let+ res : YamlWitnessType.ViolationSequence.Segment.t list = SegMap.find_opt new_node segmap in
                 (new_edge, res)
             ) nexts in
-          assert (List.length potential_nodes == 1); (* TODO: there might be more than one node *)
+          assert (List.length potential_nodes = 1); (* TODO: there might be more than one node *)
           List.hd potential_nodes
         in
 
@@ -223,7 +223,7 @@ struct
   let get_unreachable_path lines (path: (Node.t * inline_edge * Node.t) list) (segToPathMap, segments) node_to_stack =
     let has_no_branching_before_unreachable segments seg_nr =
       let rec check i: YamlWitnessType.ViolationSequence.Segment.t list -> bool = function
-        | _ when i == seg_nr -> true
+        | _ when i = seg_nr -> true
         | [] -> true
         | {segment = {waypoint_type = Branching _} :: _} :: _ -> false
         | _ :: rest -> check (i + 1) rest
@@ -254,7 +254,7 @@ struct
 
     match extract_unreach_seg_nr lines with
     | Some seg_nr when has_no_branching_before_unreachable segments seg_nr ->
-      (* TODO: consider seg_nr == 0 separately *)
+      (* TODO: consider seg_nr = 0 separately *)
       let path_suffix = SegNrToPathMap.find (List.length segments - seg_nr -1) segToPathMap in
       if not (is_within_loop (List.hd path_suffix)) && not (has_setjump_calls path) then path_suffix
       else path

From f6f8817db71934a1dd76eb531708118ce3e13a9f Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 7 Jul 2025 13:11:06 +0300
Subject: [PATCH 25/73] Bugfix: consider also Ret edges when removing function
 calls from callstack

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

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 5a8016b3ec..420ff40fcd 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -318,7 +318,7 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod
       let new_stack = match edge with
         | MyARG.CFGEdge (Entry f) when f.svar.vname <> "main" -> node :: prev_stack
         | InlineEntry _ -> node :: prev_stack
-        | InlineReturn _ -> BatList.drop 1 prev_stack
+        | InlineReturn _ | MyARG.CFGEdge (Ret _) -> BatList.drop 1 prev_stack
         | _ -> prev_stack
       in
       Hashtbl.replace node_to_stack next_node new_stack;

From 5ec6ae78fb722ae75f6d8b7c93d0983287be23fa Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 7 Jul 2025 14:07:20 +0300
Subject: [PATCH 26/73] Bugfix: check that none of the function calls from the
 callstack are within a loop

---
 src/arg/violation.ml | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 420ff40fcd..d54443f230 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -232,15 +232,16 @@ struct
     in
 
     let is_within_loop (node, _, _) =
-      let callstack = List.rev (Hashtbl.find node_to_stack node) in (* TODO: inefficient rev *)
-      let cfg_node = match callstack with
-        | hd :: _ -> Node.cfgnode hd
-        | [] -> Node.cfgnode node
-      in
+      let callstack = Hashtbl.find_opt node_to_stack node |> Option.value ~default:[] in
       let scc_components = CfgTools.node_scc_global in
-      match CfgTools.NH.find_option scc_components cfg_node with
-      | Some scc when CfgTools.NH.length scc.nodes > 1 -> true
-      | _ -> false
+
+      let is_in_loop node =
+        match CfgTools.NH.find_option scc_components (Node.cfgnode node) with
+        | Some scc when CfgTools.NH.length scc.nodes > 1 -> true
+        | _ -> false
+      in
+
+      List.exists is_in_loop callstack
     in
 
     let has_setjump_calls (path: (Node.t * inline_edge * Node.t) list): bool =

From 798d41f2f283427cf0daf8c9c06c7f306617f02d Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 7 Jul 2025 14:44:34 +0300
Subject: [PATCH 27/73] Move `collect_callstack` from `bfs` to
 `get_unreachable_path`

and only consider  `InlineEntry` and `InlineReturn` without `Entry` and `Ret` for creating the callstack
---
 src/arg/violation.ml | 49 ++++++++++++++++++++++----------------------
 1 file changed, 25 insertions(+), 24 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index d54443f230..738e830975 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -41,7 +41,7 @@ sig
     | Infeasible of (Node.t * MyARG.inline_edge * Node.t) list
     | Unknown
 
-  val check_path: (Node.t * MyARG.inline_edge * Node.t) list -> (Node.t, Node.t list) Hashtbl.t -> result
+  val check_path: (Node.t * MyARG.inline_edge * Node.t) list -> result
 end
 
 module CfgNode = Node
@@ -220,7 +220,22 @@ struct
     let command = Printf.sprintf "%s --witness-check %s %s --guide-only %s" witch witness_file_path data_model files in
     read_command_output command
 
-  let get_unreachable_path lines (path: (Node.t * inline_edge * Node.t) list) (segToPathMap, segments) node_to_stack =
+  let get_unreachable_path lines (path: (Node.t * inline_edge * Node.t) list) (segToPathMap, segments) =
+    let module NHT = BatHashtbl.Make (Arg.Node) in
+    let node_to_stack = NHT.create 100 in
+
+    let collect_callstack node edge next_node =
+      let prev_stack = NHT.find_option node_to_stack node |> Option.value ~default:[] in
+      let new_stack = match edge with
+        | InlineEntry _ -> node :: prev_stack
+        | InlineReturn _ -> BatList.drop 1 prev_stack
+        | _ -> prev_stack
+      in
+      NHT.replace node_to_stack next_node new_stack;
+    in
+
+    List.iter (fun (node, edge, next_node) -> collect_callstack node edge next_node) path;
+
     let has_no_branching_before_unreachable segments seg_nr =
       let rec check i: YamlWitnessType.ViolationSequence.Segment.t list -> bool = function
         | _ when i = seg_nr -> true
@@ -232,7 +247,7 @@ struct
     in
 
     let is_within_loop (node, _, _) =
-      let callstack = Hashtbl.find_opt node_to_stack node |> Option.value ~default:[] in
+      let callstack = NHT.find_option node_to_stack node |> Option.value ~default:[] in
       let scc_components = CfgTools.node_scc_global in
 
       let is_in_loop node =
@@ -268,14 +283,14 @@ struct
     | Some _ -> Unknown
     | None -> Unknown
 
-  let check_path path node_to_stack =
+  let check_path path =
     let seg = write path in
     let witch = GobConfig.get_string "exp.witch" in
     match witch with
     | "" -> Unknown
     | _ ->
       let lines = run_witch witch in
-      let path = get_unreachable_path lines path seg node_to_stack in
+      let path = get_unreachable_path lines path seg in
       check_feasability_with_witch lines path
 end
 
@@ -312,18 +327,6 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod
   let find_path nodes =
     let next_nodes = NHT.create 100 in
     let itered_nodes = NHT.create 100 in
-    let node_to_stack = Hashtbl.create 100 in
-
-    let collect_callstack node edge next_node =
-      let prev_stack = Hashtbl.find_opt node_to_stack node |> Option.value ~default:[] in
-      let new_stack = match edge with
-        | MyARG.CFGEdge (Entry f) when f.svar.vname <> "main" -> node :: prev_stack
-        | InlineEntry _ -> node :: prev_stack
-        | InlineReturn _ | MyARG.CFGEdge (Ret _) -> BatList.drop 1 prev_stack
-        | _ -> prev_stack
-      in
-      Hashtbl.replace node_to_stack next_node new_stack;
-    in
 
     let rec bfs curs nexts = match curs with
       | node :: curs' ->
@@ -336,10 +339,8 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod
               | MyARG.CFGEdge _
               | InlineEntry _
               | InlineReturn _ ->
-                if not (NHT.mem itered_nodes next_node) then (
+                if not (NHT.mem itered_nodes next_node) then
                   NHT.replace next_nodes next_node (edge, node);
-                  collect_callstack node edge next_node
-                );
                 Some next_node
               | InlinedEdge _
               | ThreadEntry _ -> None
@@ -357,13 +358,13 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod
 
     try bfs nodes []; None with
     | Found violation ->
-      Some ((List.rev_map (fun (n1, e, n2) -> (n2, e, n1)) (trace_path next_nodes violation)), node_to_stack) (* TODO: inefficient rev *)
+      Some (List.rev_map (fun (n1, e, n2) -> (n2, e, n1)) (trace_path next_nodes violation)) (* TODO: inefficient rev *)
     in
 
     begin match find_path [Arg.main_entry] with
-    | Some (path, node_to_stack) ->
-      print_path path;
-      begin match Feasibility.check_path path node_to_stack with
+      | Some path ->
+        print_path path;
+        begin match Feasibility.check_path path with
         | Feasibility.Feasible ->
           Logs.debug "feasible";
 

From b5600cf5fef897999e8592e09fd59c061bc24181 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 7 Jul 2025 15:40:18 +0300
Subject: [PATCH 28/73] Refactor: move `has_setjump_calls` check earlier

---
 src/arg/violation.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 738e830975..64dc4efe9f 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -269,10 +269,10 @@ struct
     in
 
     match extract_unreach_seg_nr lines with
-    | Some seg_nr when has_no_branching_before_unreachable segments seg_nr ->
+    | Some seg_nr when has_no_branching_before_unreachable segments seg_nr && not (has_setjump_calls path) ->
       (* TODO: consider seg_nr = 0 separately *)
       let path_suffix = SegNrToPathMap.find (List.length segments - seg_nr -1) segToPathMap in
-      if not (is_within_loop (List.hd path_suffix)) && not (has_setjump_calls path) then path_suffix
+      if not (is_within_loop (List.hd path_suffix)) then path_suffix
       else path
     | _ -> path
 

From 4f1ec2aee9801b133d709a2371fae506ded75707 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 8 Jul 2025 21:13:02 +0300
Subject: [PATCH 29/73] Bugfix: include the step preceding the unreachable node
 (as identified by Witch) in the path suffix when trimming the path

---
 src/arg/violation.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 64dc4efe9f..43da1305fd 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -272,7 +272,8 @@ struct
     | Some seg_nr when has_no_branching_before_unreachable segments seg_nr && not (has_setjump_calls path) ->
       (* TODO: consider seg_nr = 0 separately *)
       let path_suffix = SegNrToPathMap.find (List.length segments - seg_nr -1) segToPathMap in
-      if not (is_within_loop (List.hd path_suffix)) then path_suffix
+      let path_suffix_plus_one = BatList.drop (List.length path - List.length path_suffix -1) path in
+      if not (is_within_loop (List.hd path_suffix_plus_one)) then path_suffix_plus_one
       else path
     | _ -> path
 

From 4e6e78e94c92ed1e30dd62dfad4ce0fef9499915 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 8 Jul 2025 21:14:48 +0300
Subject: [PATCH 30/73] Bugfix: check loop containment for unreachable node
 itself, not just its callstack

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

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 43da1305fd..f5e7bdf447 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -256,7 +256,7 @@ struct
         | _ -> false
       in
 
-      List.exists is_in_loop callstack
+      List.exists is_in_loop (node :: callstack)
     in
 
     let has_setjump_calls (path: (Node.t * inline_edge * Node.t) list): bool =

From 842ef8d9ffd52b8eeefcc7f8f94bf1026ee85542 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Wed, 9 Jul 2025 22:18:13 +0300
Subject: [PATCH 31/73] Add branching waypoints at loop heads by considering
 loop locations for `Test` edges

---
 src/arg/violation.ml | 20 +++++++++++++++-----
 1 file changed, 15 insertions(+), 5 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index f5e7bdf447..5b7188c683 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -86,9 +86,8 @@ struct
       if YamlWitness.entry_type_enabled YamlWitnessType.ViolationSequence.entry_type then (
         let open GobOption.Syntax in
 
-        let loc prev =
+        let loc prev location =
           let cfgNode = Node.cfgnode prev in
-          let+ location = WitnessInvariant.location_location cfgNode in
           let fundec = CfgNode.find_fundec cfgNode in
           let location_function = fundec.svar.vname in
           YamlWitness.Entry.location ~location ~location_function
@@ -113,13 +112,22 @@ struct
           *)
           | MyARG.CFGEdge Ret (None, _) -> None
           | MyARG.CFGEdge Test (_, b) ->
-            let+ location = loc prev in
+            let cfgNode = Node.cfgnode prev in
+            let+ location =
+              match WitnessInvariant.location_location cfgNode, WitnessInvariant.loop_location cfgNode with
+              | None, None -> None
+              | Some l1, Some l2 -> assert (CilType.Location.equal l1 l2); Some (loc prev l1)
+              | Some l, None
+              | None, Some l -> Some (loc prev l)
+            in
             let constraint_ = constraint_ ~value:(String (Bool.to_string b)) in
             let branching = branching ~location ~action:"follow" ~constraint_ in
             let waypoints = [waypoint ~waypoint_type:(Branching branching)] in
             segment ~waypoints
           | _ ->
-            let+ location = loc prev in
+            let cfgNode = Node.cfgnode prev in
+            let+ l = WitnessInvariant.location_location cfgNode in
+            let location = loc prev l in
             let constraint_ = constraint_ ~value:(String "1") in
             let assumption = assumption ~location ~constraint_ in
             let waypoints = [waypoint ~waypoint_type:(Assumption assumption)] in
@@ -143,7 +151,9 @@ struct
           match path with
           | [] -> SegMap.empty, segToPathMap, 0
           | [(prev, edge, node)] as sub_path ->
-            let target = segment ~waypoints:[waypoint ~waypoint_type:(Target (violation_target ~location:(Option.get (loc node))))] in
+            let cfgNode = Node.cfgnode node in
+            let l = Option.get (WitnessInvariant.location_location cfgNode) in
+            let target = segment ~waypoints:[waypoint ~waypoint_type:(Target (violation_target ~location:(loc node l)))] in
             let this_seg, segToPathMap, segNr = match segment_for_edge prev edge with
               | Some seg ->
                 let segToPathMap1 = SegNrToPathMap.add 0 sub_path segToPathMap in

From 7ca25fa443b3fbd87b1298c4578fa2a2b317182e Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Wed, 9 Jul 2025 22:20:22 +0300
Subject: [PATCH 32/73] Count the number of times Witch runs

---
 src/arg/violation.ml   | 3 +++
 src/witness/witness.ml | 1 +
 2 files changed, 4 insertions(+)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 5b7188c683..11783b0dd2 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -1,6 +1,8 @@
 (** Violation checking in an ARG. *)
 open MyARG
 
+let witch_runs = ref 0
+
 module type ViolationArg =
 sig
   include MyARG.S with module Edge = MyARG.InlineEdge
@@ -296,6 +298,7 @@ struct
 
   let check_path path =
     let seg = write path in
+    incr witch_runs;
     let witch = GobConfig.get_string "exp.witch" in
     match witch with
     | "" -> Unknown
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 88d71fa4ed..9c83a5bedf 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -262,6 +262,7 @@ struct
     print_task_result result
 
   let write yaml_validate_result entrystates =
+    Logs.info "Witch runs: %d" !Violation.witch_runs;
     match !AnalysisState.verified, !AnalysisState.unsound_both_branches_dead with
     | _, Some true -> print_svcomp_result "ERROR (both branches dead)"
     | Some false, _ -> print_svcomp_result "ERROR (verify)"

From 3f3cbdc1e581ffaa1b1446b5a04f77c81840e23c Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 10 Jul 2025 12:10:54 +0300
Subject: [PATCH 33/73] Print number of Witch runs only once when SV-COMP
 result is printed

---
 src/arg/violation.ml   | 2 +-
 src/witness/witness.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 11783b0dd2..281aa102bb 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -290,6 +290,7 @@ struct
     | _ -> path
 
   let check_feasability_with_witch lines path =
+    incr witch_runs;
     match extract_result_line lines with
     | Some result when String.starts_with ~prefix:"true" result -> Printf.printf "Verification result: %s\n" result; Infeasible path
     | Some result when String.starts_with ~prefix:"false" result -> Printf.printf "Verification result: %s\n" result; Feasible
@@ -298,7 +299,6 @@ struct
 
   let check_path path =
     let seg = write path in
-    incr witch_runs;
     let witch = GobConfig.get_string "exp.witch" in
     match witch with
     | "" -> Unknown
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 9c83a5bedf..583c7dc944 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -54,6 +54,7 @@ let write_file filename (module Task:Task) (module Arg: MyARG.S with type Edge.t
 
 
 let print_svcomp_result (s: string): unit =
+  Logs.info "Witch runs: %d" !Violation.witch_runs;
   Logs.result "SV-COMP result: %s" s
 
 let print_task_result result: unit =
@@ -262,7 +263,6 @@ struct
     print_task_result result
 
   let write yaml_validate_result entrystates =
-    Logs.info "Witch runs: %d" !Violation.witch_runs;
     match !AnalysisState.verified, !AnalysisState.unsound_both_branches_dead with
     | _, Some true -> print_svcomp_result "ERROR (both branches dead)"
     | Some false, _ -> print_svcomp_result "ERROR (verify)"

From c112d2dda0ff6007df833178bf51aeefd2ce55d1 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 10 Jul 2025 17:38:56 +0300
Subject: [PATCH 34/73] Add branching "false" waypoints when the path skips the
 loop entirely

---
 src/arg/violation.ml | 40 ++++++++++++++++++++++++++--------------
 1 file changed, 26 insertions(+), 14 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 281aa102bb..a7f6db262f 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -95,7 +95,19 @@ struct
           YamlWitness.Entry.location ~location ~location_function
         in
 
-        let segment_for_edge prev edge =
+        let segment_for_edge ((prev, edge, node) as path_elem) prev_path_elem =
+          let check_if_skips_loop () =
+            let nodes_in_same_loop_scc (prev, _, node) =
+              let scc_of n = CfgTools.NH.find_option CfgTools.node_scc_global (Node.cfgnode n) in
+              match scc_of prev, scc_of node with
+              | Some scc1, Some scc2 -> CfgTools.SCC.equal scc1 scc2
+              | _ -> false
+            in
+            match prev_path_elem with
+            | Some prev_path_elem -> not (nodes_in_same_loop_scc path_elem || nodes_in_same_loop_scc prev_path_elem)
+            | _ -> false
+          in
+
           match edge with
           (* TODO: Correct locations for function entry and return are currently unavailable.
              As specified by the Witness 2.0 format, these locations must point to
@@ -117,10 +129,10 @@ struct
             let cfgNode = Node.cfgnode prev in
             let+ location =
               match WitnessInvariant.location_location cfgNode, WitnessInvariant.loop_location cfgNode with
-              | None, None -> None
-              | Some l1, Some l2 -> assert (CilType.Location.equal l1 l2); Some (loc prev l1)
-              | Some l, None
-              | None, Some l -> Some (loc prev l)
+              | Some l1, Some l2 when b = false && check_if_skips_loop () -> assert (CilType.Location.equal l1 l2); Some (loc prev l1)
+              | _, Some l when b = false && check_if_skips_loop () -> Some (loc prev l)
+              | Some l, _ -> Some (loc prev l)
+              | _ -> None
             in
             let constraint_ = constraint_ ~value:(String (Bool.to_string b)) in
             let branching = branching ~location ~action:"follow" ~constraint_ in
@@ -143,20 +155,20 @@ struct
               | MyARG.InlinedEdge _ -> None
               | _ ->
                 let+ res : YamlWitnessType.ViolationSequence.Segment.t list = SegMap.find_opt new_node segmap in
-                (new_edge, res)
+                (new_edge, res, new_node)
             ) nexts in
           assert (List.length potential_nodes = 1); (* TODO: there might be more than one node *)
           List.hd potential_nodes
         in
 
-        let rec build_segments path segToPathMap segNr =
+        let rec build_segments path segToPathMap segNr ~prev_path_elem =
           match path with
           | [] -> SegMap.empty, segToPathMap, 0
-          | [(prev, edge, node)] as sub_path ->
+          | [(prev, edge, node) as path_elem] as sub_path ->
             let cfgNode = Node.cfgnode node in
             let l = Option.get (WitnessInvariant.location_location cfgNode) in
             let target = segment ~waypoints:[waypoint ~waypoint_type:(Target (violation_target ~location:(loc node l)))] in
-            let this_seg, segToPathMap, segNr = match segment_for_edge prev edge with
+            let this_seg, segToPathMap, segNr = match segment_for_edge path_elem prev_path_elem with
               | Some seg ->
                 let segToPathMap1 = SegNrToPathMap.add 0 sub_path segToPathMap in
                 let segToPathMap2 = SegNrToPathMap.add 1 sub_path segToPathMap1 in
@@ -166,17 +178,17 @@ struct
             in
             let segmap = SegMap.singleton node [target] in
             SegMap.add prev this_seg segmap, segToPathMap, segNr
-          | (prev, edge, node) :: rest as sub_path ->
-            let segmap, segToPathMap, segNr = build_segments rest segToPathMap segNr in
-            let new_edge, uncilled = find_next_segment prev edge node segmap in
-            let this_seg, segToPathMap, segNr = match segment_for_edge prev new_edge with
+          | (prev, edge, node) as path_elem :: rest as sub_path ->
+            let segmap, segToPathMap, segNr = build_segments rest segToPathMap segNr ~prev_path_elem:(Some path_elem) in
+            let new_edge, uncilled, new_node = find_next_segment prev edge node segmap in
+            let this_seg, segToPathMap, segNr = match segment_for_edge (prev, new_edge, new_node) prev_path_elem with
               | Some seg -> seg :: uncilled, SegNrToPathMap.add segNr sub_path segToPathMap, segNr + 1
               | None -> uncilled, segToPathMap, segNr
             in
             SegMap.add prev this_seg segmap, segToPathMap, segNr
         in
 
-        let segmap, segToPathMap, _ = build_segments path SegNrToPathMap.empty 0 in
+        let segmap, segToPathMap, _ = build_segments path SegNrToPathMap.empty 0 ~prev_path_elem:None in
         let segments =
           match path with
           | [] -> []

From 99433a3b3fc2acc20eaa14c0fc2509a5c2b68d32 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 10 Jul 2025 17:41:14 +0300
Subject: [PATCH 35/73] Do not add waypoints inside loops

---
 src/arg/violation.ml | 80 +++++++++++++++++++++++---------------------
 1 file changed, 42 insertions(+), 38 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index a7f6db262f..b3cb134647 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -95,10 +95,11 @@ struct
           YamlWitness.Entry.location ~location ~location_function
         in
 
+        let scc_of n = CfgTools.NH.find_option CfgTools.node_scc_global (Node.cfgnode n) in
+
         let segment_for_edge ((prev, edge, node) as path_elem) prev_path_elem =
           let check_if_skips_loop () =
             let nodes_in_same_loop_scc (prev, _, node) =
-              let scc_of n = CfgTools.NH.find_option CfgTools.node_scc_global (Node.cfgnode n) in
               match scc_of prev, scc_of node with
               | Some scc1, Some scc2 -> CfgTools.SCC.equal scc1 scc2
               | _ -> false
@@ -108,44 +109,47 @@ struct
             | _ -> false
           in
 
-          match edge with
-          (* TODO: Correct locations for function entry and return are currently unavailable.
-             As specified by the Witness 2.0 format, these locations must point to
-             the closing parenthesis after the function's parameter list.
-          *)
-          (*
-          | MyARG.InlineEntry _ ->
-            let function_enter = function_enter ~location ~action:"follow" in
-            let waypoints = [waypoint ~waypoint_type:(FunctionEnter function_enter)] in
-            segment ~waypoints
-          | MyARG.InlineReturn _ ->
-            let constraint_ = constraint_ ~value:(String "1") in
-            let function_return = function_return ~location ~action:"follow" ~constraint_ in
-            let waypoints = [waypoint ~waypoint_type:(FunctionReturn function_return)] in
-            segment ~waypoints
-          *)
-          | MyARG.CFGEdge Ret (None, _) -> None
-          | MyARG.CFGEdge Test (_, b) ->
-            let cfgNode = Node.cfgnode prev in
-            let+ location =
-              match WitnessInvariant.location_location cfgNode, WitnessInvariant.loop_location cfgNode with
-              | Some l1, Some l2 when b = false && check_if_skips_loop () -> assert (CilType.Location.equal l1 l2); Some (loc prev l1)
-              | _, Some l when b = false && check_if_skips_loop () -> Some (loc prev l)
-              | Some l, _ -> Some (loc prev l)
-              | _ -> None
-            in
-            let constraint_ = constraint_ ~value:(String (Bool.to_string b)) in
-            let branching = branching ~location ~action:"follow" ~constraint_ in
-            let waypoints = [waypoint ~waypoint_type:(Branching branching)] in
-            segment ~waypoints
+          match scc_of node with
+          | Some scc2 when CfgTools.NH.length scc2.nodes > 1 -> None
           | _ ->
-            let cfgNode = Node.cfgnode prev in
-            let+ l = WitnessInvariant.location_location cfgNode in
-            let location = loc prev l in
-            let constraint_ = constraint_ ~value:(String "1") in
-            let assumption = assumption ~location ~constraint_ in
-            let waypoints = [waypoint ~waypoint_type:(Assumption assumption)] in
-            segment ~waypoints
+            match edge with
+            (* TODO: Correct locations for function entry and return are currently unavailable.
+               As specified by the Witness 2.0 format, these locations must point to
+               the closing parenthesis after the function's parameter list.
+            *)
+            (*
+            | MyARG.InlineEntry _ ->
+              let function_enter = function_enter ~location ~action:"follow" in
+              let waypoints = [waypoint ~waypoint_type:(FunctionEnter function_enter)] in
+              segment ~waypoints
+            | MyARG.InlineReturn _ ->
+              let constraint_ = constraint_ ~value:(String "1") in
+              let function_return = function_return ~location ~action:"follow" ~constraint_ in
+              let waypoints = [waypoint ~waypoint_type:(FunctionReturn function_return)] in
+              segment ~waypoints
+            *)
+            | MyARG.CFGEdge Ret (None, _) -> None
+            | MyARG.CFGEdge Test (_, b) ->
+              let cfgNode = Node.cfgnode prev in
+              let+ location =
+                match WitnessInvariant.location_location cfgNode, WitnessInvariant.loop_location cfgNode with
+                | Some l1, Some l2 when b = false && check_if_skips_loop () -> assert (CilType.Location.equal l1 l2); Some (loc prev l1)
+                | _, Some l when b = false && check_if_skips_loop () -> Some (loc prev l)
+                | Some l, _ -> Some (loc prev l)
+                | _ -> None
+              in
+              let constraint_ = constraint_ ~value:(String (Bool.to_string b)) in
+              let branching = branching ~location ~action:"follow" ~constraint_ in
+              let waypoints = [waypoint ~waypoint_type:(Branching branching)] in
+              segment ~waypoints
+            | _ ->
+              let cfgNode = Node.cfgnode prev in
+              let+ l = WitnessInvariant.location_location cfgNode in
+              let location = loc prev l in
+              let constraint_ = constraint_ ~value:(String "1") in
+              let assumption = assumption ~location ~constraint_ in
+              let waypoints = [waypoint ~waypoint_type:(Assumption assumption)] in
+              segment ~waypoints
         in
 
         let find_next_segment prev edge node segmap =

From 1e0500745f773a3647325d52a5cd73eaa925b7cb Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Fri, 11 Jul 2025 14:01:29 +0300
Subject: [PATCH 36/73] Make the `uncil` option work again

---
 src/arg/argTools.ml | 12 +++++++++---
 src/arg/myARG.ml    |  4 ++--
 2 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/src/arg/argTools.ml b/src/arg/argTools.ml
index 1abc009ab0..e83e6de47c 100644
--- a/src/arg/argTools.ml
+++ b/src/arg/argTools.ml
@@ -211,11 +211,17 @@ struct
       let next = witness_next
     end
     in
+    let module Arg =
+      (val if GobConfig.get_bool "exp.arg.uncil" then
+          let open MyARG in
+          (module Intra (UnCilTernaryIntra (UnCilLogicIntra (CfgIntra (FileCfg.Cfg)))) (Arg): MyARG.S with type Node.t = Arg.Node.t and type Edge.t = Arg.Edge.t)
+        else
+          (module Arg)
+      )
+    in
     let module Arg =
     struct
-      open MyARG
-      module ArgIntra = CfgIntra (FileCfg.Cfg) (* TODO: put UnCilTernaryIntra and UnCilLogicIntra back so that the uncil option works *)
-      include Intra (ArgIntra) (Arg)
+      include Arg
 
       let prev = witness_prev
 
diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index 22a066c82e..d73ae86dda 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -307,7 +307,7 @@ struct
 
 
   let rec next_opt' n = match n with
-    | Statement {sid; skind=If _; _} when GobConfig.get_bool "exp.arg.uncil" ->
+    | Statement {sid; skind=If _; _} ->
       let (e, if_true_next_n,  if_false_next_n) = 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? *)
@@ -361,7 +361,7 @@ struct
       Question(e_cond, e_true, e_false, Cilfacade.typeOf e_false)
 
   let next_opt' n = match n with
-    | Statement {skind=If _; _} when GobConfig.get_bool "exp.arg.uncil" ->
+    | Statement {skind=If _; _} ->
       let (e_cond, if_true_next_n, if_false_next_n) = 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

From 05feff9abc1a146de97e551fbee5595408f954b7 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Fri, 11 Jul 2025 14:06:19 +0300
Subject: [PATCH 37/73] Only print the nr of witch runs if Witch path is set

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

diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 583c7dc944..6814b1f012 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -54,7 +54,7 @@ let write_file filename (module Task:Task) (module Arg: MyARG.S with type Edge.t
 
 
 let print_svcomp_result (s: string): unit =
-  Logs.info "Witch runs: %d" !Violation.witch_runs;
+  if GobConfig.get_string "exp.witch" <> "" then Logs.info "Witch runs: %d" !Violation.witch_runs;
   Logs.result "SV-COMP result: %s" s
 
 let print_task_result result: unit =

From 8abcc1573a89ec30d9aa03d33cf5e3e644ed1fe3 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 11 Jul 2025 17:03:31 +0300
Subject: [PATCH 38/73] Add tests where ARG uncilling crashes due to path
 sensitivity

---
 tests/sv-comp/cfg/uncil/and_ambiguous1.c      |  13 ++
 .../sv-comp/cfg/uncil/and_ambiguous1.expected |   1 +
 tests/sv-comp/cfg/uncil/and_ambiguous2.c      |  13 ++
 .../sv-comp/cfg/uncil/and_ambiguous2.expected |   1 +
 tests/sv-comp/dune.inc                        | 126 ++++++++++++------
 tests/sv-comp/gen/gen.ml                      |   2 +-
 6 files changed, 114 insertions(+), 42 deletions(-)
 create mode 100644 tests/sv-comp/cfg/uncil/and_ambiguous1.c
 create mode 100644 tests/sv-comp/cfg/uncil/and_ambiguous1.expected
 create mode 100644 tests/sv-comp/cfg/uncil/and_ambiguous2.c
 create mode 100644 tests/sv-comp/cfg/uncil/and_ambiguous2.expected

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..1333ed77b7
--- /dev/null
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous1.expected
@@ -0,0 +1 @@
+TODO
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..1333ed77b7
--- /dev/null
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous2.expected
@@ -0,0 +1 @@
+TODO
diff --git a/tests/sv-comp/dune.inc b/tests/sv-comp/dune.inc
index 5ef014aec7..c5074f088b 100644
--- a/tests/sv-comp/dune.inc
+++ b/tests/sv-comp/dune.inc
@@ -12,7 +12,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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 svcomp.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)))))
 
@@ -726,6 +726,50 @@
   (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 svcomp.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 svcomp.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
@@ -738,7 +782,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp.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 svcomp.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 +804,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp.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 svcomp.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)))))
 
@@ -782,7 +826,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp.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 svcomp.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 +848,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp.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 svcomp.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 +870,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp.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 svcomp.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 +892,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp.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 svcomp.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 +914,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp.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 svcomp.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 +936,7 @@
   (action
    (progn
     (ignore-outputs
-     (run goblint --conf svcomp.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 svcomp.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 2b2cbfcdd3..748a27e8b4 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 svcomp.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 svcomp.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)))))
 

From 063faa618cd773eede13959fc94a194654c8f7f0 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 11 Jul 2025 17:45:54 +0300
Subject: [PATCH 39/73] Hack ARG uncilling to remember and follow paths to
 avoid move_opt

---
 src/arg/myARG.ml | 67 ++++++++++++++++++++++++++++++------------------
 1 file changed, 42 insertions(+), 25 deletions(-)

diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index 22a066c82e..8cd4679179 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -19,7 +19,7 @@ end
 
 module type Edge =
 sig
-  type t
+  type t [@@deriving eq]
 
   val embed: MyCFG.edge -> t
   val to_string: t -> string
@@ -27,7 +27,7 @@ end
 
 module CFGEdge: Edge with type t = MyCFG.edge =
 struct
-  type t = edge
+  type t = Edge.t [@@deriving eq]
 
   let embed e = e
   let to_string e = GobPretty.sprint Edge.pretty_plain e
@@ -102,7 +102,7 @@ end
 
 module InlineEdge: Edge with type t = inline_edge =
 struct
-  type t = inline_edge
+  type t = inline_edge [@@deriving eq]
 
   let embed e = CFGEdge e
   let to_string e = InlineEdgePrintable.show e
@@ -249,13 +249,13 @@ end
 
 module type SIntra =
 sig
-  val next: MyCFG.node -> (MyCFG.edge * MyCFG.node) list
+  val next: MyCFG.node -> (MyCFG.edge * MyCFG.node * (MyCFG.edge * MyCFG.node) list) list
 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 * (MyCFG.edge * MyCFG.node) list) list) option
 end
 
 module CfgIntra (Cfg:CfgForward): SIntraOpt =
@@ -264,21 +264,21 @@ 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
+      | (Test (_, b'), _, _) when b = b' -> true
+      | (_, _, _) -> false
     ) if_next_n
   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)
+  | (Test (e_true, true), if_true_next_n, if_true_next_p), (Test (e_false, false), if_false_next_n, if_false_next_p) when Basetype.CilExp.equal e_true e_false ->
+    (e_true, (if_true_next_n, if_true_next_p), (if_false_next_n, if_false_next_p))
   | _, _ -> failwith "partition_if_next: bad branches"
 
 module UnCilLogicIntra (Arg: SIntraOpt): SIntraOpt =
@@ -286,7 +286,7 @@ struct
   open Cil
   (* TODO: questionable (=) and (==) use here *)
 
-  let is_equiv_stmtkind sk1 sk2 = match sk1, sk2 with
+  (* 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 *)
@@ -303,12 +303,14 @@ struct
   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
+    | _, _-> false *)
 
+  let rec is_equiv_chain n1 n2 =
+    Node.equal n1 n2
 
   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_p), (if_false_next_n, if_false_next_p)) = 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? *)
@@ -317,24 +319,26 @@ 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
+          let (e2, (if_true_next_true_next_n, if_true_next_true_next_p), (if_true_next_false_next_n, if_true_next_false_next_p)) = 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 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, if_true_next_p @ if_true_next_true_next_p);
+              (Test (exp, false), if_true_next_false_next_n, if_true_next_p @ if_true_next_false_next_p);
+              (Test (exp, false), if_false_next_n, if_false_next_p)
             ]
           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
+          let (e2, (if_false_next_true_next_n, if_false_next_true_next_p), (if_false_next_false_next_n, if_false_next_false_next_p)) = 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 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_true_next_n, if_true_next_p);
+              (Test (exp, true), if_false_next_true_next_n, if_false_next_p @ if_false_next_true_next_p);
+              (Test (exp, false), if_false_next_false_next_n, if_false_next_p @ if_false_next_false_next_p)
             ]
           else
             None
@@ -362,14 +366,15 @@ 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_p), (if_false_next_n, if_false_next_p)) = 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_p)], [(Assign (v_false, e_false), if_false_next_next_n, if_false_next_next_p)] 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, if_true_next_p @ if_true_next_next_p);
+            (Assign (v_false, exp), if_false_next_next_n, if_false_next_p @ if_false_next_next_p)
           ]
         | _, _ -> None
       else
@@ -388,14 +393,26 @@ module Intra (ArgIntra: SIntraOpt) (Arg: S):
 struct
   include Arg
 
+  (* let rec follow node to_n p = Node.move_opt node to_n *)
+  let rec follow node to_n 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' to_n 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+ to_node = follow node to_n p in
           (Edge.embed e, to_node)
         )
 end

From 67e4cefa7e55480a101d47338afa1004d3d1fd9e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 11 Jul 2025 17:51:15 +0300
Subject: [PATCH 40/73] Fix ARG uncilling hack duplicating edges

---
 src/arg/myARG.ml                              |  7 +++--
 .../sv-comp/cfg/uncil/and_ambiguous1.expected | 28 ++++++++++++++++++-
 .../sv-comp/cfg/uncil/and_ambiguous2.expected | 28 ++++++++++++++++++-
 3 files changed, 58 insertions(+), 5 deletions(-)

diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index 8cd4679179..ef4eac6738 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -19,7 +19,7 @@ end
 
 module type Edge =
 sig
-  type t [@@deriving eq]
+  type t [@@deriving eq, ord]
 
   val embed: MyCFG.edge -> t
   val to_string: t -> string
@@ -27,7 +27,7 @@ end
 
 module CFGEdge: Edge with type t = MyCFG.edge =
 struct
-  type t = Edge.t [@@deriving eq]
+  type t = Edge.t [@@deriving eq, ord]
 
   let embed e = e
   let to_string e = GobPretty.sprint Edge.pretty_plain e
@@ -102,7 +102,7 @@ end
 
 module InlineEdge: Edge with type t = inline_edge =
 struct
-  type t = inline_edge [@@deriving eq]
+  type t = inline_edge [@@deriving eq, ord]
 
   let embed e = CFGEdge e
   let to_string e = InlineEdgePrintable.show e
@@ -415,4 +415,5 @@ struct
           let+ to_node = follow node to_n p in
           (Edge.embed e, to_node)
         )
+      |> BatList.unique_cmp ~cmp:[%ord: Edge.t * Node.t] (* TODO: avoid generating duplicates in the first place? *)
 end
diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous1.expected b/tests/sv-comp/cfg/uncil/and_ambiguous1.expected
index 1333ed77b7..560abd05c3 100644
--- a/tests/sv-comp/cfg/uncil/and_ambiguous1.expected
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous1.expected
@@ -1 +1,27 @@
-TODO
+                             ┌──────────────────────────────────┐
+                             │                _                 │
+                             └──────────────────────────────────┘
+                               │
+                               │ 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.expected b/tests/sv-comp/cfg/uncil/and_ambiguous2.expected
index 1333ed77b7..1cbc9466a2 100644
--- a/tests/sv-comp/cfg/uncil/and_ambiguous2.expected
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous2.expected
@@ -1 +1,27 @@
-TODO
+                             ┌──────────────────────────────────┐
+                             │                _                 │
+                             └──────────────────────────────────┘
+                               │
+                               │ 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)      │
+  └────────────────────────▶ │                _                 │ ◀────────────────────────┘
+                             └──────────────────────────────────┘

From 6333f93eadc0499af8a7a124540919e8f4efb384 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 11 Sep 2025 13:40:52 +0300
Subject: [PATCH 41/73] Consider all possible paths in `next_opt`

---
 src/arg/myARG.ml | 70 +++++++++++++++++++++++++++++++-----------------
 1 file changed, 46 insertions(+), 24 deletions(-)

diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index 8c725606f7..c0f991aa4a 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -268,18 +268,43 @@ struct
   let next_opt _ = None
 end
 
-let partition_if_next if_next_n =
+type path = (edge * node) list
+let cartesian_concat_paths (ps : path list) (qs : path list) : path list = List.concat (List.map (fun p -> List.map (fun q -> p @ q) qs) ps)
+let mk_edges (e : edge) (n : node) (paths : path list) : (edge * node * path) list = List.map (fun p -> (e, n, p)) paths
+let combine_and_make (e : edge) (n : node) (lhs : path list) (rhs : path list) : (edge * node * path) list = mk_edges e n (cartesian_concat_paths lhs rhs)
+
+let partition_if_next (if_next_n : (edge * node * (edge * node) list) list): exp * (node * path list) * (node * path list) =
   (* 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 exp =
+    match if_next_n with
+    | [] -> failwith "partition_if_next: empty"
+    | (Test (exp, _), _, _) :: xs ->
+      let all_tests_same_cond =
+        List.for_all
+          (function
+            | (Test (exp', _), _, _) -> Basetype.CilExp.equal exp exp'
+            | _ -> false)
+          xs
+      in
+      if all_tests_same_cond then exp
+      else failwith "partition_if_next: bad branches"
+    | _ -> failwith "partition_if_next: not Test edge"
+  in
+  let collapse_branch b =
+    let paths_for_b = List.filter (function
+        | (Test (_, b'), _, _) when b = b' -> true
+        | _ -> false)
+        if_next_n
+    in
+    match paths_for_b with
+    | [] -> failwith (if b then "partition_if_next: missing true-branch" else "partition_if_next: missing false-branch")
+    | (e, n, p) :: rest ->
+      let all_same_en = List.for_all (fun (e', n', _) -> Edge.equal e e' && Node.equal n n') paths_for_b in
+      if not all_same_en then failwith "partition_if_next: branch has differing (edge,node) pairs";
+      let paths = List.map (fun (_,_,p) -> p) paths_for_b in
+      (n, paths)
   in
-  (* assert (List.length if_next <= 2); *)
-  match test_next true, test_next false with
-  | (Test (e_true, true), if_true_next_n, if_true_next_p), (Test (e_false, false), if_false_next_n, if_false_next_p) when Basetype.CilExp.equal e_true e_false ->
-    (e_true, (if_true_next_n, if_true_next_p), (if_false_next_n, if_false_next_p))
-  | _, _ -> failwith "partition_if_next: bad branches"
+  (exp, collapse_branch true, collapse_branch false)
 
 module UnCilLogicIntra (Arg: SIntraOpt): SIntraOpt =
 struct
@@ -323,11 +348,10 @@ struct
           let (e2, (if_true_next_true_next_n, if_true_next_true_next_p), (if_true_next_false_next_n, if_true_next_false_next_p)) = 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 exp = BinOp (LAnd, e, e2, intType) in
-            Some [
-              (Test (exp, true), if_true_next_true_next_n, if_true_next_p @ if_true_next_true_next_p);
-              (Test (exp, false), if_true_next_false_next_n, if_true_next_p @ if_true_next_false_next_p);
-              (Test (exp, false), if_false_next_n, if_false_next_p)
-            ]
+            let true_items = combine_and_make (Test (exp, true)) if_true_next_true_next_n if_true_next_p if_true_next_true_next_p in
+            let false_from_true_items = combine_and_make (Test (exp, false)) if_true_next_false_next_n if_true_next_p if_true_next_false_next_p in
+            let false_from_false_items = mk_edges (Test (exp, false)) if_false_next_n if_false_next_p in
+            Some (true_items @ false_from_true_items @ false_from_false_items)
           else
             None
         (* || *)
@@ -336,11 +360,10 @@ struct
           let (e2, (if_false_next_true_next_n, if_false_next_true_next_p), (if_false_next_false_next_n, if_false_next_false_next_p)) = 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 exp = BinOp (LOr, e, e2, intType) in
-            Some [
-              (Test (exp, true), if_true_next_n, if_true_next_p);
-              (Test (exp, true), if_false_next_true_next_n, if_false_next_p @ if_false_next_true_next_p);
-              (Test (exp, false), if_false_next_false_next_n, if_false_next_p @ if_false_next_false_next_p)
-            ]
+            let true_from_true_items = mk_edges (Test (exp, true)) if_true_next_n if_true_next_p in
+            let true_from_false_items = combine_and_make (Test (exp, true)) if_false_next_true_next_n if_false_next_p if_false_next_true_next_p in
+            let false_from_false_items = combine_and_make (Test (exp, false)) if_false_next_false_next_n if_false_next_p if_false_next_false_next_p in
+            Some (true_from_true_items @ true_from_false_items @ false_from_false_items)
           else
             None
         | _, _ -> None
@@ -373,10 +396,9 @@ struct
         match Arg.next if_true_next_n, Arg.next if_false_next_n with
         | [(Assign (v_true, e_true), if_true_next_next_n, if_true_next_next_p)], [(Assign (v_false, e_false), if_false_next_next_n, if_false_next_next_p)] 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, if_true_next_p @ if_true_next_next_p);
-            (Assign (v_false, exp), if_false_next_next_n, if_false_next_p @ if_false_next_next_p)
-          ]
+          let assigns_true = combine_and_make (Assign (v_true, exp)) if_true_next_next_n if_true_next_p [if_true_next_next_p] in
+          let assigns_false = combine_and_make (Assign (v_false, exp)) if_false_next_next_n if_false_next_p [if_false_next_next_p] in
+          Some (assigns_true @ assigns_false)
         | _, _ -> None
       else
         None

From 0604c03b6d34cae4883970ec7395e0a05e5ecb7a Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 16 Oct 2025 16:00:06 +0300
Subject: [PATCH 42/73] Update configuration to the one used for server runs

---
 conf/svcomp25.json | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/conf/svcomp25.json b/conf/svcomp25.json
index 9d4081cbe0..f7b7fec7ee 100644
--- a/conf/svcomp25.json
+++ b/conf/svcomp25.json
@@ -65,16 +65,19 @@
         "congruence",
         "octagon",
         "wideningThresholds",
-        "loopUnrollHeuristic",
         "memsafetySpecification",
         "noOverflows",
         "termination",
         "tmpSpecialAnalysis"
       ]
-    }
+    },
+    "wp": true
   },
   "exp": {
-    "region-offsets": true
+    "region-offsets": true,
+    "arg": {
+      "enabled": true
+    }
   },
   "solver": "td3",
   "sem": {
@@ -90,10 +93,11 @@
   },
   "witness": {
     "yaml": {
-      "enabled": true,
+      "enabled": false,
       "format-version": "2.0",
       "entry-types": [
-        "invariant_set"
+        "invariant_set",
+        "violation_sequence"
       ],
       "invariant-types": [
         "loop_invariant"
@@ -102,7 +106,7 @@
     "invariant": {
       "loop-head": true,
       "after-lock": false,
-      "other": false,
+      "other": true,
       "accessed": false,
       "exact": true
     }

From 9677dd4497a8059fdfedc2fcc76174c4238a388a Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 4 Nov 2025 15:56:22 +0200
Subject: [PATCH 43/73] Adapt Witch command to new witness-producing Witch

---
 src/arg/violation.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index b3cb134647..c9132f455b 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -243,9 +243,11 @@ struct
       | "32bit" -> "--32"
       | _ -> failwith "invalid architecture"
     in
+    let property = GobConfig.get_string "ana.specification" in
     let witness_file_path = GobConfig.get_string "witness.yaml.path" in
     (*  ../witch/scripts/symbiotic --witness-check ../analyzer/witness.yml --32 ../analyzer/violation-witness.c *)
-    let command = Printf.sprintf "%s --witness-check %s %s --guide-only %s" witch witness_file_path data_model files in
+    let witch_path_s = Fpath.to_string (Fpath.append GobSys.exe_dir (Fpath.v witch)) in
+    let command = Printf.sprintf "%s --witness-check %s --witness %s --prp %s %s --guide-only %s" witch_path_s witness_file_path witness_file_path property data_model files in
     read_command_output command
 
   let get_unreachable_path lines (path: (Node.t * inline_edge * Node.t) list) (segToPathMap, segments) =

From 86d696fc2218b2c17c0c7ec5014ff275b5fd9c7b Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Fri, 7 Nov 2025 14:04:03 +0200
Subject: [PATCH 44/73] Use the cilled path prefix of the corresponding
 uncilling to determine the correct node for segmap lookup

---
 src/arg/myARG.ml     | 28 ++++++++++++++++++++++++++--
 src/arg/violation.ml | 24 ++++++++++++------------
 2 files changed, 38 insertions(+), 14 deletions(-)

diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index b2047b16cc..f1c0beded4 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -430,8 +430,7 @@ struct
     | None -> Arg.next n
 end
 
-module Intra (ArgIntra: SIntraOpt) (Arg: S):
-  S with module Node = Arg.Node and module Edge = Arg.Edge =
+module Intra (ArgIntra: SIntraOpt) (Arg: S) =
 struct
   include Arg
 
@@ -447,6 +446,18 @@ struct
       in
       follow node' to_n p'
 
+  let rec follow' (node : Node.t) to_n p : (Node.t * (Edge.t * Node.t) list) list =
+    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
+      let+ (n, l) = follow' node' to_n p' in
+      (n, (Edge.embed e, node') :: l)
+
   let next node =
     let open GobList.Syntax in
     match ArgIntra.next_opt (Node.cfgnode node) with
@@ -458,4 +469,17 @@ struct
           (Edge.embed e, to_node)
         )
       |> BatList.unique_cmp ~cmp:[%ord: Edge.t * Node.t] (* TODO: avoid generating duplicates in the first place? *)
+
+  let next' node =
+    let open GobList.Syntax in
+    match ArgIntra.next_opt (Node.cfgnode node) with
+    | None ->
+      Arg.next node
+      |> List.map (fun (e,n) -> (e,n, [e, n]))
+    | Some next ->
+      next
+      |> BatList.concat_map (fun (e, to_n, p) ->
+          let+ (to_node, path) = follow' node to_n p in
+          (Edge.embed e, to_node, path)
+        )
 end
diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index c9132f455b..ffdec8459e 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -152,17 +152,17 @@ struct
               segment ~waypoints
         in
 
-        let find_next_segment prev edge node segmap =
-          let nexts = UnCilArg.next prev in
-          let potential_nodes = List.filter_map (fun (new_edge, new_node) ->
-              match new_edge with
-              | MyARG.InlinedEdge _ -> None
-              | _ ->
-                let+ res : YamlWitnessType.ViolationSequence.Segment.t list = SegMap.find_opt new_node segmap in
-                (new_edge, res, new_node)
-            ) nexts in
-          assert (List.length potential_nodes = 1); (* TODO: there might be more than one node *)
-          List.hd potential_nodes
+        let find_next_segment prev edge node segmap (sub_path : (Node.t * inline_edge * Node.t) list) =
+          let rec is_prefix prefix full =
+            match prefix, full with
+            | [], _ -> true
+            | _, [] -> false
+            | (e,n)::xs, (_, e1, n1)::ys -> Node.equal n n1 && Arg.Edge.equal e e1 && is_prefix xs ys
+          in
+          let nexts = UnCilArg.next' prev in
+          let (new_edge, new_node, p) as res = List.find (fun (_, _, p) -> is_prefix p sub_path) nexts in
+          let res = SegMap.find_opt new_node segmap in
+          (new_edge, Option.get res, new_node)
         in
 
         let rec build_segments path segToPathMap segNr ~prev_path_elem =
@@ -184,7 +184,7 @@ struct
             SegMap.add prev this_seg segmap, segToPathMap, segNr
           | (prev, edge, node) as path_elem :: rest as sub_path ->
             let segmap, segToPathMap, segNr = build_segments rest segToPathMap segNr ~prev_path_elem:(Some path_elem) in
-            let new_edge, uncilled, new_node = find_next_segment prev edge node segmap in
+            let new_edge, uncilled, new_node = find_next_segment prev edge node segmap sub_path in
             let this_seg, segToPathMap, segNr = match segment_for_edge (prev, new_edge, new_node) prev_path_elem with
               | Some seg -> seg :: uncilled, SegNrToPathMap.add segNr sub_path segToPathMap, segNr + 1
               | None -> uncilled, segToPathMap, segNr

From f037fa2dd4afcbc5af97620420f98382adfab4d8 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Fri, 7 Nov 2025 14:18:25 +0200
Subject: [PATCH 45/73] Refactor

---
 src/arg/violation.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index ffdec8459e..9cb5a39011 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -152,7 +152,7 @@ struct
               segment ~waypoints
         in
 
-        let find_next_segment prev edge node segmap (sub_path : (Node.t * inline_edge * Node.t) list) =
+        let uncil prev (sub_path : (Node.t * inline_edge * Node.t) list) =
           let rec is_prefix prefix full =
             match prefix, full with
             | [], _ -> true
@@ -160,15 +160,14 @@ struct
             | (e,n)::xs, (_, e1, n1)::ys -> Node.equal n n1 && Arg.Edge.equal e e1 && is_prefix xs ys
           in
           let nexts = UnCilArg.next' prev in
-          let (new_edge, new_node, p) as res = List.find (fun (_, _, p) -> is_prefix p sub_path) nexts in
-          let res = SegMap.find_opt new_node segmap in
-          (new_edge, Option.get res, new_node)
+          let (new_edge, new_node, p) = List.find (fun (_, _, p) -> is_prefix p sub_path) nexts in
+          (new_edge, new_node)
         in
 
         let rec build_segments path segToPathMap segNr ~prev_path_elem =
           match path with
           | [] -> SegMap.empty, segToPathMap, 0
-          | [(prev, edge, node) as path_elem] as sub_path ->
+          | [(prev, _, node) as path_elem] as sub_path ->
             let cfgNode = Node.cfgnode node in
             let l = Option.get (WitnessInvariant.location_location cfgNode) in
             let target = segment ~waypoints:[waypoint ~waypoint_type:(Target (violation_target ~location:(loc node l)))] in
@@ -182,12 +181,13 @@ struct
             in
             let segmap = SegMap.singleton node [target] in
             SegMap.add prev this_seg segmap, segToPathMap, segNr
-          | (prev, edge, node) as path_elem :: rest as sub_path ->
+          | (prev, _, _) as path_elem :: rest as sub_path ->
             let segmap, segToPathMap, segNr = build_segments rest segToPathMap segNr ~prev_path_elem:(Some path_elem) in
-            let new_edge, uncilled, new_node = find_next_segment prev edge node segmap sub_path in
+            let new_edge, new_node = uncil prev sub_path in
+            let segments = Option.get (SegMap.find_opt new_node segmap) in
             let this_seg, segToPathMap, segNr = match segment_for_edge (prev, new_edge, new_node) prev_path_elem with
-              | Some seg -> seg :: uncilled, SegNrToPathMap.add segNr sub_path segToPathMap, segNr + 1
-              | None -> uncilled, segToPathMap, segNr
+              | Some seg -> seg :: segments, SegNrToPathMap.add segNr sub_path segToPathMap, segNr + 1
+              | None -> segments, segToPathMap, segNr
             in
             SegMap.add prev this_seg segmap, segToPathMap, segNr
         in

From 6ce92576f323a1a03b9a39d14d4bf44b86d41d29 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Sun, 9 Nov 2025 01:12:29 +0200
Subject: [PATCH 46/73] Remove branching waypoints with invalid locations using
 Witch

---
 src/arg/violation.ml | 77 ++++++++++++++++++++++++++++++--------------
 1 file changed, 52 insertions(+), 25 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 9cb5a39011..d9aaffeec1 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -59,6 +59,18 @@ struct
     | Infeasible of (Node.t * MyARG.inline_edge * Node.t) list
     | Unknown
 
+  open YamlWitness.Entry
+  (* TODO: duplicate code copied from YamlWitness.write *)
+  let input_files = GobConfig.get_string_list "files"
+  let data_model = match GobConfig.get_string "exp.architecture" with
+    | "64bit" -> "LP64"
+    | "32bit" -> "ILP32"
+    | _ -> failwith "invalid architecture"
+  let specification = Option.map (fun (module Task: Svcomp.Task) ->
+      Svcomp.Specification.to_string Task.specification
+    ) !Svcomp.task
+  let task = task ~input_files ~data_model ~specification
+
   let write (path : (Node.t * MyARG.inline_edge * Node.t) list) =
     let module FileCfg =
     struct
@@ -68,26 +80,12 @@ struct
     let module WitnessInvariant = WitnessUtil.YamlInvariant (FileCfg) in
     let module UnCilArg = Intra (UnCilTernaryIntra (UnCilLogicIntra (CfgIntra (FileCfg.Cfg)))) (Arg) in
 
-    let open YamlWitness.Entry in
-    (* TODO: duplicate code copied from YamlWitness.write *)
-    let input_files = GobConfig.get_string_list "files" in
-    let data_model = match GobConfig.get_string "exp.architecture" with
-      | "64bit" -> "LP64"
-      | "32bit" -> "ILP32"
-      | _ -> failwith "invalid architecture"
-    in
-    let specification = Option.map (fun (module Task: Svcomp.Task) ->
-        Svcomp.Specification.to_string Task.specification
-      ) !Svcomp.task
-    in
-    let task = task ~input_files ~data_model ~specification in
-
-    let entries = [] in
-
-    let entries, segToPathMap, segments =
+    let entries, segToPathMap, segments, has_branching =
       if YamlWitness.entry_type_enabled YamlWitnessType.ViolationSequence.entry_type then (
         let open GobOption.Syntax in
 
+        let has_branching = ref false in
+
         let loc prev location =
           let cfgNode = Node.cfgnode prev in
           let fundec = CfgNode.find_fundec cfgNode in
@@ -141,6 +139,7 @@ struct
               let constraint_ = constraint_ ~value:(String (Bool.to_string b)) in
               let branching = branching ~location ~action:"follow" ~constraint_ in
               let waypoints = [waypoint ~waypoint_type:(Branching branching)] in
+              has_branching := true;
               segment ~waypoints
             | _ ->
               let cfgNode = Node.cfgnode prev in
@@ -200,16 +199,16 @@ struct
         in
 
         let entry = YamlWitness.Entry.violation_sequence ~task ~violation:segments in
-        [entry], segToPathMap, segments
+        [entry], segToPathMap, segments, !has_branching
       )
       else
-        entries, SegNrToPathMap.empty, []
+        [], SegNrToPathMap.empty, [], false
     in
 
     let yaml_entries = List.rev_map YamlWitnessType.Entry.to_yaml entries in
     (* TODO: "witness generation summary" message *)
     YamlWitness.yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path"));
-    segToPathMap, segments
+    (segToPathMap, segments), has_branching
 
   let read_command_output command =
     let (ic, _) as process = Unix.open_process command in
@@ -228,6 +227,19 @@ struct
     let re = Str.regexp "^RESULT: \\(.*\\)$" in
     List.find_map (fun line -> if Str.string_match re line 0 then Some (Str.matched_group 1 line) else None) lines
 
+  let extract_invalid_locations lines =
+  let re = Str.regexp "^INFO: Found invalid locations in segments \\[\\(.*\\)\\]$" in
+  List.find_map
+    (fun line ->
+       if Str.string_match re line 0 then
+         let inside = Str.matched_group 1 line in
+         let parts = Str.split (Str.regexp "[ ,]+") inside in
+         let nums = parts |> List.filter (fun s -> s <> "") |> List.map int_of_string in
+         Some nums
+       else
+         None)
+    lines
+
   (* TODO: find both (result and seg nr) with one traversal *)
   let extract_unreach_seg_nr lines =
     let re = Str.regexp "segment \\([0-9]+\\) cannot be passed" in
@@ -236,7 +248,7 @@ struct
         with Not_found -> None
       ) lines
 
-  let run_witch witch =
+  let run_witch check_locs =
     let files = String.concat " " (GobConfig.get_string_list "files") in
     let data_model = match GobConfig.get_string "exp.architecture" with
       | "64bit" -> "--64"
@@ -245,9 +257,10 @@ struct
     in
     let property = GobConfig.get_string "ana.specification" in
     let witness_file_path = GobConfig.get_string "witness.yaml.path" in
+    let check_locs_flag = if check_locs then "--check-all-locations" else "" in
     (*  ../witch/scripts/symbiotic --witness-check ../analyzer/witness.yml --32 ../analyzer/violation-witness.c *)
-    let witch_path_s = Fpath.to_string (Fpath.append GobSys.exe_dir (Fpath.v witch)) in
-    let command = Printf.sprintf "%s --witness-check %s --witness %s --prp %s %s --guide-only %s" witch_path_s witness_file_path witness_file_path property data_model files in
+    let witch_path_s = Fpath.to_string (Fpath.append GobSys.exe_dir (Fpath.v (GobConfig.get_string "exp.witch"))) in
+    let command = Printf.sprintf "%s --witness-check %s --witness %s --prp %s %s %s --guide-only %s" witch_path_s witness_file_path witness_file_path property data_model check_locs_flag files in
     read_command_output command
 
   let get_unreachable_path lines (path: (Node.t * inline_edge * Node.t) list) (segToPathMap, segments) =
@@ -307,6 +320,19 @@ struct
       else path
     | _ -> path
 
+  let check_and_remove_invalid_locs (segToPathMap, segments) =
+    let lines = run_witch true in
+    match extract_invalid_locations lines with
+    | Some seg_nrs ->
+      let segments' = List.filteri (fun i _ -> not @@ List.mem i seg_nrs) segments in
+      let entries = [YamlWitness.Entry.violation_sequence ~task ~violation:segments'] in
+      let yaml_entries = List.rev_map YamlWitnessType.Entry.to_yaml entries in
+      (* TODO: "witness generation summary" message *)
+      YamlWitness.yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path"));
+      segToPathMap, segments'
+    | _ ->
+      segToPathMap, segments
+
   let check_feasability_with_witch lines path =
     incr witch_runs;
     match extract_result_line lines with
@@ -316,12 +342,13 @@ struct
     | None -> Unknown
 
   let check_path path =
-    let seg = write path in
+    let seg, has_branching = write path in
     let witch = GobConfig.get_string "exp.witch" in
     match witch with
     | "" -> Unknown
     | _ ->
-      let lines = run_witch witch in
+      let seg = if has_branching then check_and_remove_invalid_locs seg else seg in
+      let lines = run_witch false in
       let path = get_unreachable_path lines path seg in
       check_feasability_with_witch lines path
 end

From cc6af51e7161c2b18f52acf8e7c359fc00f03729 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 10 Nov 2025 14:20:52 +0200
Subject: [PATCH 47/73] Do not run Witch twice if result is already found
 during the location checks

---
 src/arg/violation.ml | 38 ++++++++++++++++++++++----------------
 1 file changed, 22 insertions(+), 16 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index d9aaffeec1..66de2058cf 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -320,7 +320,15 @@ struct
       else path
     | _ -> path
 
-  let check_and_remove_invalid_locs (segToPathMap, segments) =
+  let check_feasability_with_witch lines path =
+    match extract_result_line lines with
+    | Some result when String.starts_with ~prefix:"true" result -> Printf.printf "Verification result: %s\n" result; Infeasible path
+    | Some result when String.starts_with ~prefix:"false" result -> Printf.printf "Verification result: %s\n" result; Feasible
+    | Some _ -> Unknown
+    | None -> Unknown
+
+  let check_and_remove_invalid_locs (segToPathMap, segments) path =
+    incr witch_runs;
     let lines = run_witch true in
     match extract_invalid_locations lines with
     | Some seg_nrs ->
@@ -329,17 +337,11 @@ struct
       let yaml_entries = List.rev_map YamlWitnessType.Entry.to_yaml entries in
       (* TODO: "witness generation summary" message *)
       YamlWitness.yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path"));
-      segToPathMap, segments'
-    | _ ->
-      segToPathMap, segments
-
-  let check_feasability_with_witch lines path =
-    incr witch_runs;
-    match extract_result_line lines with
-    | Some result when String.starts_with ~prefix:"true" result -> Printf.printf "Verification result: %s\n" result; Infeasible path
-    | Some result when String.starts_with ~prefix:"false" result -> Printf.printf "Verification result: %s\n" result; Feasible
-    | Some _ -> Unknown
-    | None -> Unknown
+      let seg = segToPathMap, segments' in
+      let lines = run_witch false in
+      let path = get_unreachable_path lines path seg in
+      check_feasability_with_witch lines path
+    | _ -> check_feasability_with_witch lines path
 
   let check_path path =
     let seg, has_branching = write path in
@@ -347,10 +349,14 @@ struct
     match witch with
     | "" -> Unknown
     | _ ->
-      let seg = if has_branching then check_and_remove_invalid_locs seg else seg in
-      let lines = run_witch false in
-      let path = get_unreachable_path lines path seg in
-      check_feasability_with_witch lines path
+      if has_branching then
+        check_and_remove_invalid_locs seg path
+      else (
+        incr witch_runs;
+        let lines = run_witch false in
+        let path = get_unreachable_path lines path seg in
+        check_feasability_with_witch lines path
+      )
 end
 
 

From afe27f58d4fdace03be1efce7538f186ad53aa5a Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 10 Nov 2025 14:44:57 +0200
Subject: [PATCH 48/73] Refactor

---
 src/arg/violation.ml | 33 +++++++++++++++++----------------
 1 file changed, 17 insertions(+), 16 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 66de2058cf..4205bc1b17 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -248,7 +248,8 @@ struct
         with Not_found -> None
       ) lines
 
-  let run_witch check_locs =
+  let run_witch ~check_locs =
+    incr witch_runs;
     let files = String.concat " " (GobConfig.get_string_list "files") in
     let data_model = match GobConfig.get_string "exp.architecture" with
       | "64bit" -> "--64"
@@ -327,9 +328,7 @@ struct
     | Some _ -> Unknown
     | None -> Unknown
 
-  let check_and_remove_invalid_locs (segToPathMap, segments) path =
-    incr witch_runs;
-    let lines = run_witch true in
+  let check_and_remove_invalid_locs lines path (segToPathMap, segments as seg) =
     match extract_invalid_locations lines with
     | Some seg_nrs ->
       let segments' = List.filteri (fun i _ -> not @@ List.mem i seg_nrs) segments in
@@ -337,11 +336,14 @@ struct
       let yaml_entries = List.rev_map YamlWitnessType.Entry.to_yaml entries in
       (* TODO: "witness generation summary" message *)
       YamlWitness.yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path"));
-      let seg = segToPathMap, segments' in
-      let lines = run_witch false in
-      let path = get_unreachable_path lines path seg in
-      check_feasability_with_witch lines path
-    | _ -> check_feasability_with_witch lines path
+      let seg' = (segToPathMap, segments') in
+      let lines' = run_witch ~check_locs:false in
+      lines', seg'
+    | _ -> lines, seg
+
+  let process_witch_output lines path seg =
+    let unreachable_path = get_unreachable_path lines path seg in
+    check_feasability_with_witch lines unreachable_path
 
   let check_path path =
     let seg, has_branching = write path in
@@ -350,13 +352,12 @@ struct
     | "" -> Unknown
     | _ ->
       if has_branching then
-        check_and_remove_invalid_locs seg path
-      else (
-        incr witch_runs;
-        let lines = run_witch false in
-        let path = get_unreachable_path lines path seg in
-        check_feasability_with_witch lines path
-      )
+        let lines = run_witch ~check_locs:true in
+        let lines', seg' = check_and_remove_invalid_locs lines path seg in
+        process_witch_output lines' path seg'
+      else
+        let lines = run_witch ~check_locs:false in
+        process_witch_output lines path seg
 end
 
 

From 78eaa50bd0774e9f61027460d5d744004bdb8d32 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 10 Nov 2025 14:48:27 +0200
Subject: [PATCH 49/73] Optimize

---
 src/arg/violation.ml | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 4205bc1b17..39a2074589 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -321,9 +321,9 @@ struct
       else path
     | _ -> path
 
-  let check_feasability_with_witch lines path =
+  let check_feasability_with_witch lines path seg =
     match extract_result_line lines with
-    | Some result when String.starts_with ~prefix:"true" result -> Printf.printf "Verification result: %s\n" result; Infeasible path
+    | Some result when String.starts_with ~prefix:"true" result -> Printf.printf "Verification result: %s\n" result; Infeasible (get_unreachable_path lines path seg)
     | Some result when String.starts_with ~prefix:"false" result -> Printf.printf "Verification result: %s\n" result; Feasible
     | Some _ -> Unknown
     | None -> Unknown
@@ -341,10 +341,6 @@ struct
       lines', seg'
     | _ -> lines, seg
 
-  let process_witch_output lines path seg =
-    let unreachable_path = get_unreachable_path lines path seg in
-    check_feasability_with_witch lines unreachable_path
-
   let check_path path =
     let seg, has_branching = write path in
     let witch = GobConfig.get_string "exp.witch" in
@@ -354,10 +350,10 @@ struct
       if has_branching then
         let lines = run_witch ~check_locs:true in
         let lines', seg' = check_and_remove_invalid_locs lines path seg in
-        process_witch_output lines' path seg'
+        check_feasability_with_witch lines' path seg'
       else
         let lines = run_witch ~check_locs:false in
-        process_witch_output lines path seg
+        check_feasability_with_witch lines path seg
 end
 
 

From 275d60b2faa020bac607c87653cc6076cc0579d5 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 27 Nov 2025 13:02:58 +0200
Subject: [PATCH 50/73] Fix indentation in `violation.ml`

---
 src/arg/violation.ml | 32 ++++++++++++++++----------------
 1 file changed, 16 insertions(+), 16 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 39a2074589..acc469a0c1 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -228,17 +228,17 @@ struct
     List.find_map (fun line -> if Str.string_match re line 0 then Some (Str.matched_group 1 line) else None) lines
 
   let extract_invalid_locations lines =
-  let re = Str.regexp "^INFO: Found invalid locations in segments \\[\\(.*\\)\\]$" in
-  List.find_map
-    (fun line ->
-       if Str.string_match re line 0 then
-         let inside = Str.matched_group 1 line in
-         let parts = Str.split (Str.regexp "[ ,]+") inside in
-         let nums = parts |> List.filter (fun s -> s <> "") |> List.map int_of_string in
-         Some nums
-       else
-         None)
-    lines
+    let re = Str.regexp "^INFO: Found invalid locations in segments \\[\\(.*\\)\\]$" in
+    List.find_map
+      (fun line ->
+         if Str.string_match re line 0 then
+           let inside = Str.matched_group 1 line in
+           let parts = Str.split (Str.regexp "[ ,]+") inside in
+           let nums = parts |> List.filter (fun s -> s <> "") |> List.map int_of_string in
+           Some nums
+         else
+           None)
+      lines
 
   (* TODO: find both (result and seg nr) with one traversal *)
   let extract_unreach_seg_nr lines =
@@ -421,12 +421,12 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod
     try bfs nodes []; None with
     | Found violation ->
       Some (List.rev_map (fun (n1, e, n2) -> (n2, e, n1)) (trace_path next_nodes violation)) (* TODO: inefficient rev *)
-    in
+  in
 
-    begin match find_path [Arg.main_entry] with
-      | Some path ->
-        print_path path;
-        begin match Feasibility.check_path path with
+  begin match find_path [Arg.main_entry] with
+    | Some path ->
+      print_path path;
+      begin match Feasibility.check_path path with
         | Feasibility.Feasible ->
           Logs.debug "feasible";
 

From 852f546afe0907df3d2b0cb89490f5cbea578284 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 27 Nov 2025 13:41:30 +0200
Subject: [PATCH 51/73] Address semgrep warnings

---
 src/arg/myARG.ml     | 2 +-
 src/arg/violation.ml | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index f1c0beded4..b2f0a137ab 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -288,7 +288,7 @@ struct
 end
 
 type path = (edge * node) list
-let cartesian_concat_paths (ps : path list) (qs : path list) : path list = List.concat (List.map (fun p -> List.map (fun q -> p @ q) qs) ps)
+let cartesian_concat_paths (ps : path list) (qs : path list) : path list = List.concat_map (fun p -> List.map (fun q -> p @ q) qs) ps
 let mk_edges (e : edge) (n : node) (paths : path list) : (edge * node * path) list = List.map (fun p -> (e, n, p)) paths
 let combine_and_make (e : edge) (n : node) (lhs : path list) (rhs : path list) : (edge * node * path) list = mk_edges e n (cartesian_concat_paths lhs rhs)
 
diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index acc469a0c1..49271c00f3 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -323,8 +323,8 @@ struct
 
   let check_feasability_with_witch lines path seg =
     match extract_result_line lines with
-    | Some result when String.starts_with ~prefix:"true" result -> Printf.printf "Verification result: %s\n" result; Infeasible (get_unreachable_path lines path seg)
-    | Some result when String.starts_with ~prefix:"false" result -> Printf.printf "Verification result: %s\n" result; Feasible
+    | Some result when String.starts_with ~prefix:"true" result -> Logs.info "Verification result: %s\n" result; Infeasible (get_unreachable_path lines path seg)
+    | Some result when String.starts_with ~prefix:"false" result -> Logs.info "Verification result: %s\n" result; Feasible
     | Some _ -> Unknown
     | None -> Unknown
 

From 19eb0bda1609b349710582be8c7f32a98ea367df Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Fri, 28 Nov 2025 13:56:58 +0200
Subject: [PATCH 52/73] Rename violation.t -> violation-validation.t

---
 .../{violation.t => violation-validation.t}/correct-hard.c        | 0
 .../{violation.t => violation-validation.t}/correct-hard.yml      | 0
 .../witness/{violation.t => violation-validation.t}/correct.c     | 0
 .../witness/{violation.t => violation-validation.t}/correct.yml   | 0
 .../witness/{violation.t => violation-validation.t}/incorrect.c   | 0
 .../witness/{violation.t => violation-validation.t}/incorrect.yml | 0
 .../witness/{violation.t => violation-validation.t}/run.t         | 0
 7 files changed, 0 insertions(+), 0 deletions(-)
 rename tests/regression/witness/{violation.t => violation-validation.t}/correct-hard.c (100%)
 rename tests/regression/witness/{violation.t => violation-validation.t}/correct-hard.yml (100%)
 rename tests/regression/witness/{violation.t => violation-validation.t}/correct.c (100%)
 rename tests/regression/witness/{violation.t => violation-validation.t}/correct.yml (100%)
 rename tests/regression/witness/{violation.t => violation-validation.t}/incorrect.c (100%)
 rename tests/regression/witness/{violation.t => violation-validation.t}/incorrect.yml (100%)
 rename tests/regression/witness/{violation.t => violation-validation.t}/run.t (100%)

diff --git a/tests/regression/witness/violation.t/correct-hard.c b/tests/regression/witness/violation-validation.t/correct-hard.c
similarity index 100%
rename from tests/regression/witness/violation.t/correct-hard.c
rename to tests/regression/witness/violation-validation.t/correct-hard.c
diff --git a/tests/regression/witness/violation.t/correct-hard.yml b/tests/regression/witness/violation-validation.t/correct-hard.yml
similarity index 100%
rename from tests/regression/witness/violation.t/correct-hard.yml
rename to tests/regression/witness/violation-validation.t/correct-hard.yml
diff --git a/tests/regression/witness/violation.t/correct.c b/tests/regression/witness/violation-validation.t/correct.c
similarity index 100%
rename from tests/regression/witness/violation.t/correct.c
rename to tests/regression/witness/violation-validation.t/correct.c
diff --git a/tests/regression/witness/violation.t/correct.yml b/tests/regression/witness/violation-validation.t/correct.yml
similarity index 100%
rename from tests/regression/witness/violation.t/correct.yml
rename to tests/regression/witness/violation-validation.t/correct.yml
diff --git a/tests/regression/witness/violation.t/incorrect.c b/tests/regression/witness/violation-validation.t/incorrect.c
similarity index 100%
rename from tests/regression/witness/violation.t/incorrect.c
rename to tests/regression/witness/violation-validation.t/incorrect.c
diff --git a/tests/regression/witness/violation.t/incorrect.yml b/tests/regression/witness/violation-validation.t/incorrect.yml
similarity index 100%
rename from tests/regression/witness/violation.t/incorrect.yml
rename to tests/regression/witness/violation-validation.t/incorrect.yml
diff --git a/tests/regression/witness/violation.t/run.t b/tests/regression/witness/violation-validation.t/run.t
similarity index 100%
rename from tests/regression/witness/violation.t/run.t
rename to tests/regression/witness/violation-validation.t/run.t

From bb3d696717ab52fdcfcfbd1292bbb8eb5c2850bf Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Fri, 28 Nov 2025 14:45:04 +0200
Subject: [PATCH 53/73] Add a cram test for violation witness generation

---
 .../witness/violation.t/callfpointer.c        |  21 +++
 .../witness/violation.t/callfpointer.expected |  51 ++++++++
 tests/regression/witness/violation.t/run.t    | 123 ++++++++++++++++++
 3 files changed, 195 insertions(+)
 create mode 100644 tests/regression/witness/violation.t/callfpointer.c
 create mode 100644 tests/regression/witness/violation.t/callfpointer.expected
 create mode 100644 tests/regression/witness/violation.t/run.t

diff --git a/tests/regression/witness/violation.t/callfpointer.c b/tests/regression/witness/violation.t/callfpointer.c
new file mode 100644
index 0000000000..b0d4f04bfb
--- /dev/null
+++ b/tests/regression/witness/violation.t/callfpointer.c
@@ -0,0 +1,21 @@
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "callfpointer.c", 3, "reach_error"); }
+
+
+void f(void g(int)) {
+ g(1);
+}
+
+void h(int i) {
+ if(i==1) {
+  ERROR: {reach_error();abort();}
+ } else {
+
+ }
+}
+int main(void) {
+ f(h);
+
+ return 0;
+}
diff --git a/tests/regression/witness/violation.t/callfpointer.expected b/tests/regression/witness/violation.t/callfpointer.expected
new file mode 100644
index 0000000000..aa0f4cd7d2
--- /dev/null
+++ b/tests/regression/witness/violation.t/callfpointer.expected
@@ -0,0 +1,51 @@
+┌──────────────────────┐
+│          _           │
+└──────────────────────┘
+  │
+  │ Entry main
+  ▼
+┌──────────────────────┐
+│          _           │
+└──────────────────────┘
+  │
+  │ InlineEntry '(& h)'
+  ▼
+┌──────────────────────┐
+│          _           │
+└──────────────────────┘
+  │
+  │ Entry f
+  ▼
+┌──────────────────────┐
+│          _           │
+└──────────────────────┘
+  │
+  │ InlineEntry '(1)'
+  ▼
+┌──────────────────────┐
+│          _           │
+└──────────────────────┘
+  │
+  │ Entry h
+  ▼
+┌──────────────────────┐
+│          _           │
+└──────────────────────┘
+  │
+  │ Test (i == 1,true)
+  ▼
+┌──────────────────────┐
+│          _           │
+└──────────────────────┘
+  │
+  │ InlineEntry '()'
+  ▼
+┌──────────────────────┐
+│          _           │
+└──────────────────────┘
+  │
+  │ Entry reach_error
+  ▼
+┌──────────────────────┐
+│          _           │
+└──────────────────────┘
\ No newline at end of file
diff --git a/tests/regression/witness/violation.t/run.t b/tests/regression/witness/violation.t/run.t
new file mode 100644
index 0000000000..582c81610e
--- /dev/null
+++ b/tests/regression/witness/violation.t/run.t
@@ -0,0 +1,123 @@
+  $ goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )"} callfpointer.c --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --enable ana.wp  --set witness.yaml.entry-types[+] violation_sequence --enable witness.yaml.sv-comp-true-only --enable witness.invariant.other 
+  [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
+  [Warning][Deadcode] Function 'main' does not return
+  [Warning][Deadcode] Function 'f' has dead code:
+    on line 8 (callfpointer.c:8-8)
+  [Warning][Deadcode] Function 'h' has dead code:
+    on line 16 (callfpointer.c:16-16)
+  [Warning][Deadcode] Function 'main' has dead code:
+    on line 20 (callfpointer.c:20-20)
+  [Warning][Deadcode] Logical lines of code (LLoC) summary:
+    live: 8
+    dead: 3
+    total lines: 11
+  [Warning][Deadcode][CWE-571] condition 'i == 1' is always true (callfpointer.c:11:5-11:9)
+  [Info]   fun316main(12)[7] =[Entry main]=> s11(12)[7]
+  [Info]   s11(12)[7] =[InlineEntry '(& h)']=> fun309f(18)[16]@s11(12)[7]
+  [Info]   fun309f(18)[16]@s11(12)[7] =[Entry f]=> s3(18)[16]@s11(12)[7]
+  [Info]   s3(18)[16]@s11(12)[7] =[InlineEntry '(1)']=> fun313h(24)[21]@s3(18)[16]@s11(12)[7]
+  [Info]   fun313h(24)[21]@s3(18)[16]@s11(12)[7] =[Entry h]=> s5(24)[21]@s3(18)[16]@s11(12)[7]
+  [Info]   s5(24)[21]@s3(18)[16]@s11(12)[7] =[Test (i == 1,true)]=> s7(24)[21]@s3(18)[16]@s11(12)[7]
+  SV-COMP result: unknown
+
+  $ graph-easy --as=boxart arg.dot
+  ┌──────────────────────┐
+  │          _           │
+  └──────────────────────┘
+    │
+    │ Entry main
+    ▼
+  ┌──────────────────────┐
+  │          _           │
+  └──────────────────────┘
+    │
+    │ InlineEntry '(& h)'
+    ▼
+  ┌──────────────────────┐
+  │          _           │
+  └──────────────────────┘
+    │
+    │ Entry f
+    ▼
+  ┌──────────────────────┐
+  │          _           │
+  └──────────────────────┘
+    │
+    │ InlineEntry '(1)'
+    ▼
+  ┌──────────────────────┐
+  │          _           │
+  └──────────────────────┘
+    │
+    │ Entry h
+    ▼
+  ┌──────────────────────┐
+  │          _           │
+  └──────────────────────┘
+    │
+    │ Test (i == 1,true)
+    ▼
+  ┌──────────────────────┐
+  │          _           │
+  └──────────────────────┘
+    │
+    │ InlineEntry '()'
+    ▼
+  ┌──────────────────────┐
+  │          _           │
+  └──────────────────────┘
+    │
+    │ Entry reach_error
+    ▼
+  ┌──────────────────────┐
+  │          _           │
+  └──────────────────────┘
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: violation_sequence
+    content:
+    - segment:
+      - waypoint:
+          type: assumption
+          location:
+            file_name: callfpointer.c
+            line: 18
+            column: 2
+            function: main
+          action: follow
+          constraint:
+            value: "1"
+            format: c_expression
+    - segment:
+      - waypoint:
+          type: assumption
+          location:
+            file_name: callfpointer.c
+            line: 7
+            column: 2
+            function: f
+          action: follow
+          constraint:
+            value: "1"
+            format: c_expression
+    - segment:
+      - waypoint:
+          type: branching
+          location:
+            file_name: callfpointer.c
+            line: 11
+            column: 2
+            function: h
+          action: follow
+          constraint:
+            value: "true"
+            format: c_expression
+    - segment:
+      - waypoint:
+          type: target
+          location:
+            file_name: callfpointer.c
+            line: 12
+            column: 11
+            function: h
+          action: follow

From 01fd90c055d6f0d60196f34218132f58c1d1bc5a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 11 Jul 2025 17:45:54 +0300
Subject: [PATCH 54/73] Fix ambiguous ARG uncilling crash by remembering and
 following CFG paths

---
 src/arg/myARG.ml                              | 68 ++++++++++++-------
 .../sv-comp/cfg/uncil/and_ambiguous1.expected | 28 +++++++-
 .../sv-comp/cfg/uncil/and_ambiguous2.expected | 28 +++++++-
 3 files changed, 97 insertions(+), 27 deletions(-)

diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index 22a066c82e..ef4eac6738 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -19,7 +19,7 @@ end
 
 module type Edge =
 sig
-  type t
+  type t [@@deriving eq, ord]
 
   val embed: MyCFG.edge -> t
   val to_string: t -> string
@@ -27,7 +27,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 +102,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
@@ -249,13 +249,13 @@ end
 
 module type SIntra =
 sig
-  val next: MyCFG.node -> (MyCFG.edge * MyCFG.node) list
+  val next: MyCFG.node -> (MyCFG.edge * MyCFG.node * (MyCFG.edge * MyCFG.node) list) list
 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 * (MyCFG.edge * MyCFG.node) list) list) option
 end
 
 module CfgIntra (Cfg:CfgForward): SIntraOpt =
@@ -264,21 +264,21 @@ 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
+      | (Test (_, b'), _, _) when b = b' -> true
+      | (_, _, _) -> false
     ) if_next_n
   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)
+  | (Test (e_true, true), if_true_next_n, if_true_next_p), (Test (e_false, false), if_false_next_n, if_false_next_p) when Basetype.CilExp.equal e_true e_false ->
+    (e_true, (if_true_next_n, if_true_next_p), (if_false_next_n, if_false_next_p))
   | _, _ -> failwith "partition_if_next: bad branches"
 
 module UnCilLogicIntra (Arg: SIntraOpt): SIntraOpt =
@@ -286,7 +286,7 @@ struct
   open Cil
   (* TODO: questionable (=) and (==) use here *)
 
-  let is_equiv_stmtkind sk1 sk2 = match sk1, sk2 with
+  (* 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 *)
@@ -303,12 +303,14 @@ struct
   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
+    | _, _-> false *)
 
+  let rec is_equiv_chain n1 n2 =
+    Node.equal n1 n2
 
   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_p), (if_false_next_n, if_false_next_p)) = 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? *)
@@ -317,24 +319,26 @@ 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
+          let (e2, (if_true_next_true_next_n, if_true_next_true_next_p), (if_true_next_false_next_n, if_true_next_false_next_p)) = 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 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, if_true_next_p @ if_true_next_true_next_p);
+              (Test (exp, false), if_true_next_false_next_n, if_true_next_p @ if_true_next_false_next_p);
+              (Test (exp, false), if_false_next_n, if_false_next_p)
             ]
           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
+          let (e2, (if_false_next_true_next_n, if_false_next_true_next_p), (if_false_next_false_next_n, if_false_next_false_next_p)) = 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 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_true_next_n, if_true_next_p);
+              (Test (exp, true), if_false_next_true_next_n, if_false_next_p @ if_false_next_true_next_p);
+              (Test (exp, false), if_false_next_false_next_n, if_false_next_p @ if_false_next_false_next_p)
             ]
           else
             None
@@ -362,14 +366,15 @@ 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_p), (if_false_next_n, if_false_next_p)) = 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_p)], [(Assign (v_false, e_false), if_false_next_next_n, if_false_next_next_p)] 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, if_true_next_p @ if_true_next_next_p);
+            (Assign (v_false, exp), if_false_next_next_n, if_false_next_p @ if_false_next_next_p)
           ]
         | _, _ -> None
       else
@@ -388,14 +393,27 @@ module Intra (ArgIntra: SIntraOpt) (Arg: S):
 struct
   include Arg
 
+  (* let rec follow node to_n p = Node.move_opt node to_n *)
+  let rec follow node to_n 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' to_n 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+ to_node = follow node to_n p in
           (Edge.embed e, to_node)
         )
+      |> BatList.unique_cmp ~cmp:[%ord: Edge.t * Node.t] (* TODO: avoid generating duplicates in the first place? *)
 end
diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous1.expected b/tests/sv-comp/cfg/uncil/and_ambiguous1.expected
index 1333ed77b7..560abd05c3 100644
--- a/tests/sv-comp/cfg/uncil/and_ambiguous1.expected
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous1.expected
@@ -1 +1,27 @@
-TODO
+                             ┌──────────────────────────────────┐
+                             │                _                 │
+                             └──────────────────────────────────┘
+                               │
+                               │ 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.expected b/tests/sv-comp/cfg/uncil/and_ambiguous2.expected
index 1333ed77b7..1cbc9466a2 100644
--- a/tests/sv-comp/cfg/uncil/and_ambiguous2.expected
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous2.expected
@@ -1 +1,27 @@
-TODO
+                             ┌──────────────────────────────────┐
+                             │                _                 │
+                             └──────────────────────────────────┘
+                               │
+                               │ 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)      │
+  └────────────────────────▶ │                _                 │ ◀────────────────────────┘
+                             └──────────────────────────────────┘

From 566813f72cf641eb044a7b6cd2ab6ea83697f78f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 28 Nov 2025 15:31:23 +0200
Subject: [PATCH 55/73] Comment ARG uncilling by following CFG paths

---
 src/arg/myARG.ml | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index ef4eac6738..1205db9d90 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -250,12 +250,14 @@ end
 module type SIntra =
 sig
   val next: MyCFG.node -> (MyCFG.edge * MyCFG.node * (MyCFG.edge * MyCFG.node) list) list
+  (** @return Inner list is the original CFG path corresponding to the step. *) (* TODO: extract type *)
 end
 
 module type SIntraOpt =
 sig
   include SIntra
   val next_opt: MyCFG.node -> ((MyCFG.edge * MyCFG.node * (MyCFG.edge * MyCFG.node) list) list) option
+  (** @return Inner list is the original CFG path corresponding to the step. *) (* TODO: extract type *)
 end
 
 module CfgIntra (Cfg:CfgForward): SIntraOpt =
@@ -306,7 +308,7 @@ struct
     | _, _-> false *)
 
   let rec is_equiv_chain n1 n2 =
-    Node.equal n1 n2
+    Node.equal n1 n2 (* TODO: is it fine to not detect equivalent chains anymore? if so, could inline this *)
 
   let rec next_opt' n = match n with
     | Statement {sid; skind=If _; _} when GobConfig.get_bool "exp.arg.uncil" ->
@@ -324,6 +326,7 @@ struct
             let exp = BinOp (LAnd, e, e2, intType) in
             Some [
               (Test (exp, true), if_true_next_true_next_n, if_true_next_p @ if_true_next_true_next_p);
+              (* two different paths to same false node *)
               (Test (exp, false), if_true_next_false_next_n, if_true_next_p @ if_true_next_false_next_p);
               (Test (exp, false), if_false_next_n, if_false_next_p)
             ]
@@ -336,6 +339,7 @@ struct
           if is_equiv_chain if_true_next_n if_false_next_true_next_n then
             let exp = BinOp (LOr, e, e2, intType) in
             Some [
+              (* two different paths to same true node *)
               (Test (exp, true), if_true_next_n, if_true_next_p);
               (Test (exp, true), if_false_next_true_next_n, if_false_next_p @ if_false_next_true_next_p);
               (Test (exp, false), if_false_next_false_next_n, if_false_next_p @ if_false_next_false_next_p)
@@ -393,8 +397,11 @@ module Intra (ArgIntra: SIntraOpt) (Arg: S):
 struct
   include Arg
 
-  (* let rec follow node to_n p = Node.move_opt node to_n *)
-  let rec follow node to_n p =
+  (* TODO: remove Node.move_opt? *)
+
+  (** 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 to_n p = (* TODO: to_n argument unused? *)
     let open GobList.Syntax in
     match p with
     | [] -> [node]
@@ -413,7 +420,8 @@ struct
       next
       |> BatList.concat_map (fun (e, to_n, p) ->
           let+ to_node = follow node to_n p in
+          (* TODO: what's the point of to_n? should it match to_node? *)
           (Edge.embed e, to_node)
         )
-      |> BatList.unique_cmp ~cmp:[%ord: Edge.t * Node.t] (* TODO: avoid generating duplicates in the first place? *)
+      |> 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

From b68f4e5b326993e50f29089fd421d31d63ba77f2 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 28 Nov 2025 15:47:50 +0200
Subject: [PATCH 56/73] Remove now-unused ARG Node move_opt

---
 src/arg/argTools.ml | 10 ----------
 src/arg/myARG.ml    | 10 ----------
 2 files changed, 20 deletions(-)

diff --git a/src/arg/argTools.ml b/src/arg/argTools.ml
index a220120912..f9d57d1666 100644
--- a/src/arg/argTools.ml
+++ b/src/arg/argTools.ml
@@ -138,16 +138,6 @@ struct
       | 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
diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index e15362dfaf..e32408a29f 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -13,7 +13,6 @@ sig
   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
 
@@ -131,13 +130,6 @@ struct
     |> 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
 
@@ -416,8 +408,6 @@ module Intra (ArgIntra: SIntraOpt) (Arg: S):
 struct
   include Arg
 
-  (* TODO: remove Node.move_opt? *)
-
   (** 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 to_n p = (* TODO: to_n argument unused? *)

From 60078ab752a2f298f76162b13e4a1d2f7bd154a3 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 28 Nov 2025 15:50:10 +0200
Subject: [PATCH 57/73] Remove unused ARG Node equal_node_context

Last usage was removed a long time ago in cb32b12a377ba255b02735890e4eb50afab16cca.
---
 src/arg/argTools.ml | 3 ---
 src/arg/myARG.ml    | 4 ----
 2 files changed, 7 deletions(-)

diff --git a/src/arg/argTools.ml b/src/arg/argTools.ml
index f9d57d1666..6d91fc3843 100644
--- a/src/arg/argTools.ml
+++ b/src/arg/argTools.ml
@@ -137,9 +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
-
-    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 e32408a29f..2d6c6d95e7 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -12,8 +12,6 @@ sig
   val context_id: t -> int
   val path_id: t -> int
   val to_string: t -> string
-
-  val equal_node_context: t -> t -> bool
 end
 
 module type Edge =
@@ -129,8 +127,6 @@ struct
     nl
     |> List.map Node.to_string
     |> String.concat "@"
-
-  let equal_node_context _ _ = failwith "StackNode: equal_node_context"
 end
 
 module Stack (Arg: S with module Edge = InlineEdge):

From ca40482dc008312b37e5f5315d06a0d61bfd68dc Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Fri, 28 Nov 2025 16:07:28 +0200
Subject: [PATCH 58/73] Change path printing log level to debug

---
 src/arg/violation.ml                       | 2 +-
 tests/regression/witness/violation.t/run.t | 6 ------
 2 files changed, 1 insertion(+), 7 deletions(-)

diff --git a/src/arg/violation.ml b/src/arg/violation.ml
index 49271c00f3..fb13909baa 100644
--- a/src/arg/violation.ml
+++ b/src/arg/violation.ml
@@ -380,7 +380,7 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod
 
   let print_path path =
     List.iter (fun (n1, e, n2) ->
-        Logs.info "  %s =[%s]=> %s" (Arg.Node.to_string n1) (Arg.Edge.to_string e) (Arg.Node.to_string n2)
+        Logs.debug "  %s =[%s]=> %s" (Arg.Node.to_string n1) (Arg.Edge.to_string e) (Arg.Node.to_string n2)
       ) path
   in
 
diff --git a/tests/regression/witness/violation.t/run.t b/tests/regression/witness/violation.t/run.t
index 582c81610e..a17f4cd8c3 100644
--- a/tests/regression/witness/violation.t/run.t
+++ b/tests/regression/witness/violation.t/run.t
@@ -12,12 +12,6 @@
     dead: 3
     total lines: 11
   [Warning][Deadcode][CWE-571] condition 'i == 1' is always true (callfpointer.c:11:5-11:9)
-  [Info]   fun316main(12)[7] =[Entry main]=> s11(12)[7]
-  [Info]   s11(12)[7] =[InlineEntry '(& h)']=> fun309f(18)[16]@s11(12)[7]
-  [Info]   fun309f(18)[16]@s11(12)[7] =[Entry f]=> s3(18)[16]@s11(12)[7]
-  [Info]   s3(18)[16]@s11(12)[7] =[InlineEntry '(1)']=> fun313h(24)[21]@s3(18)[16]@s11(12)[7]
-  [Info]   fun313h(24)[21]@s3(18)[16]@s11(12)[7] =[Entry h]=> s5(24)[21]@s3(18)[16]@s11(12)[7]
-  [Info]   s5(24)[21]@s3(18)[16]@s11(12)[7] =[Test (i == 1,true)]=> s7(24)[21]@s3(18)[16]@s11(12)[7]
   SV-COMP result: unknown
 
   $ graph-easy --as=boxart arg.dot

From c2bbd89737affd662b5cb8b91a16066ba2b23dcc Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 28 Nov 2025 15:54:20 +0200
Subject: [PATCH 59/73] Remove unused to_n argument in MyArg.Intra.follow

---
 src/arg/myARG.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index 2d6c6d95e7..6f21c98dc5 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -406,7 +406,7 @@ struct
 
   (** 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 to_n p = (* TODO: to_n argument unused? *)
+  let rec follow node p =
     let open GobList.Syntax in
     match p with
     | [] -> [node]
@@ -415,7 +415,7 @@ struct
           Edge.equal (Edge.embed e) e' && Node0.equal to_n (Node.cfgnode to_node)
         ) (Arg.next node)
       in
-      follow node' to_n p'
+      follow node' p'
 
   let next node =
     let open GobList.Syntax in
@@ -424,7 +424,7 @@ struct
     | Some next ->
       next
       |> BatList.concat_map (fun (e, to_n, p) ->
-          let+ to_node = follow node to_n p in
+          let+ to_node = follow node p in
           (* TODO: what's the point of to_n? should it match to_node? *)
           (Edge.embed e, to_node)
         )

From fdf177927e13eeba6e6b2a5bb1a033e20326e9c7 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 28 Nov 2025 15:56:06 +0200
Subject: [PATCH 60/73] Add assert about to_n to MyARG.Intra.next

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

diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index 6f21c98dc5..cf000c3e17 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -425,7 +425,7 @@ struct
       next
       |> BatList.concat_map (fun (e, to_n, p) ->
           let+ to_node = follow node p in
-          (* TODO: what's the point of to_n? should it match to_node? *)
+          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? *)

From 32c0acdc01cb2f07ee82213480618ee9a56ca15d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 28 Nov 2025 16:10:02 +0200
Subject: [PATCH 61/73] Remove ARG equivalent CFG chain detection

---
 src/arg/myARG.ml             | 30 +++++-------------------------
 src/common/util/cilfacade.ml |  2 +-
 2 files changed, 6 insertions(+), 26 deletions(-)

diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index cf000c3e17..22edacb25b 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -293,29 +293,9 @@ let partition_if_next if_next_n =
 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 rec is_equiv_chain n1 n2 =
-    Node.equal n1 n2 (* TODO: is it fine to not detect equivalent chains anymore? if so, could inline this *)
+
+  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" ->
@@ -329,7 +309,7 @@ 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_true_next_p), (if_true_next_false_next_n, if_true_next_false_next_p)) = partition_if_next (next if_true_next_n) in
-          if is_equiv_chain if_false_next_n if_true_next_false_next_n then
+          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, if_true_next_p @ if_true_next_true_next_p);
@@ -343,7 +323,7 @@ struct
         | _, 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_true_next_p), (if_false_next_false_next_n, if_false_next_false_next_p)) = partition_if_next (next if_false_next_n) in
-          if is_equiv_chain if_true_next_n if_false_next_true_next_n then
+          if Node.equal if_true_next_n if_false_next_true_next_n then
             let exp = BinOp (LOr, e, e2, intType) in
             Some [
               (* two different paths to same true node *)
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
 

From f85449f2ed68762e09f3f27a98560fe3087f1251 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 28 Nov 2025 16:15:28 +0200
Subject: [PATCH 62/73] Extract type MyARG.cfg_path

---
 src/arg/myARG.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index 22edacb25b..a65aa4355f 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -253,18 +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 * (MyCFG.edge * MyCFG.node) list) list
-  (** @return Inner list is the original CFG path corresponding to the step. *) (* TODO: extract type *)
+  val next: MyCFG.node -> (MyCFG.edge * MyCFG.node * cfg_path) list
+  (** @return Also the original CFG path corresponding to the step. *)
 end
 
 module type SIntraOpt =
 sig
   include SIntra
-  val next_opt: MyCFG.node -> ((MyCFG.edge * MyCFG.node * (MyCFG.edge * MyCFG.node) list) list) option
-  (** @return Inner list is the original CFG path corresponding to the step. *) (* TODO: extract type *)
+  val next_opt: MyCFG.node -> ((MyCFG.edge * MyCFG.node * cfg_path) list) option
+  (** @return Also the original CFG path corresponding to the step. *)
 end
 
 module CfgIntra (Cfg:CfgForward): SIntraOpt =

From 0f8b387ae162ced13bdc9feb86613f235c53d97d Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 1 Dec 2025 14:21:53 +0200
Subject: [PATCH 63/73] Disable violation cram tests on OSX

---
 .../witness/violation.t/callfpointer.expected | 51 -------------------
 tests/regression/witness/violation.t/dune     |  3 ++
 2 files changed, 3 insertions(+), 51 deletions(-)
 delete mode 100644 tests/regression/witness/violation.t/callfpointer.expected
 create mode 100644 tests/regression/witness/violation.t/dune

diff --git a/tests/regression/witness/violation.t/callfpointer.expected b/tests/regression/witness/violation.t/callfpointer.expected
deleted file mode 100644
index aa0f4cd7d2..0000000000
--- a/tests/regression/witness/violation.t/callfpointer.expected
+++ /dev/null
@@ -1,51 +0,0 @@
-┌──────────────────────┐
-│          _           │
-└──────────────────────┘
-  │
-  │ Entry main
-  ▼
-┌──────────────────────┐
-│          _           │
-└──────────────────────┘
-  │
-  │ InlineEntry '(& h)'
-  ▼
-┌──────────────────────┐
-│          _           │
-└──────────────────────┘
-  │
-  │ Entry f
-  ▼
-┌──────────────────────┐
-│          _           │
-└──────────────────────┘
-  │
-  │ InlineEntry '(1)'
-  ▼
-┌──────────────────────┐
-│          _           │
-└──────────────────────┘
-  │
-  │ Entry h
-  ▼
-┌──────────────────────┐
-│          _           │
-└──────────────────────┘
-  │
-  │ Test (i == 1,true)
-  ▼
-┌──────────────────────┐
-│          _           │
-└──────────────────────┘
-  │
-  │ InlineEntry '()'
-  ▼
-┌──────────────────────┐
-│          _           │
-└──────────────────────┘
-  │
-  │ Entry reach_error
-  ▼
-┌──────────────────────┐
-│          _           │
-└──────────────────────┘
\ No newline at end of file
diff --git a/tests/regression/witness/violation.t/dune b/tests/regression/witness/violation.t/dune
new file mode 100644
index 0000000000..e6194ac86b
--- /dev/null
+++ b/tests/regression/witness/violation.t/dune
@@ -0,0 +1,3 @@
+(cram
+ (applies_to run)
+ (enabled_if (<> %{system} macosx)))

From 4640382e431eec9b2f073827e716cec59e0a275d Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 1 Dec 2025 14:46:08 +0200
Subject: [PATCH 64/73] Disable violation cram tests on OSX

---
 tests/regression/dune                     | 4 ++++
 tests/regression/witness/violation.t/dune | 3 ---
 2 files changed, 4 insertions(+), 3 deletions(-)
 delete mode 100644 tests/regression/witness/violation.t/dune

diff --git a/tests/regression/dune b/tests/regression/dune
index 0fd8052478..b1e37d56fd 100644
--- a/tests/regression/dune
+++ b/tests/regression/dune
@@ -27,3 +27,7 @@
    (package goblint)
    %{bin:yamlWitnessStrip}
    %{bin:yamlWitnessStripDiff}))
+
+(cram
+ (applies_to violation)
+ (enabled_if (<> %{system} macosx)))
\ No newline at end of file
diff --git a/tests/regression/witness/violation.t/dune b/tests/regression/witness/violation.t/dune
deleted file mode 100644
index e6194ac86b..0000000000
--- a/tests/regression/witness/violation.t/dune
+++ /dev/null
@@ -1,3 +0,0 @@
-(cram
- (applies_to run)
- (enabled_if (<> %{system} macosx)))

From 29d05cfc8b7c67233c931d307d5c75c099788a8c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 1 Dec 2025 15:33:49 +0200
Subject: [PATCH 65/73] Add tests where MyARG.partition_if_next choosing
 arbitrary single path leads to unfollowable path

partition_if_next uses List.find to find one branch, but there may be multiple with different paths.
If the arbitrarily chosen path ends up being dead in the ARG, some ARG node may be missing, just because partition_if_next picked the "wrong" path.
---
 .../cfg/uncil/and_ambiguous_partition1.c      | 13 +++
 .../uncil/and_ambiguous_partition1.expected   | 33 +++++++
 .../cfg/uncil/and_ambiguous_partition2.c      | 13 +++
 .../uncil/and_ambiguous_partition2.expected   | 33 +++++++
 .../cfg/uncil/and_ambiguous_partition3.c      | 13 +++
 .../uncil/and_ambiguous_partition3.expected   | 33 +++++++
 .../cfg/uncil/and_ambiguous_partition4.c      | 13 +++
 .../uncil/and_ambiguous_partition4.expected   | 33 +++++++
 tests/sv-comp/dune.inc                        | 88 +++++++++++++++++++
 9 files changed, 272 insertions(+)
 create mode 100644 tests/sv-comp/cfg/uncil/and_ambiguous_partition1.c
 create mode 100644 tests/sv-comp/cfg/uncil/and_ambiguous_partition1.expected
 create mode 100644 tests/sv-comp/cfg/uncil/and_ambiguous_partition2.c
 create mode 100644 tests/sv-comp/cfg/uncil/and_ambiguous_partition2.expected
 create mode 100644 tests/sv-comp/cfg/uncil/and_ambiguous_partition3.c
 create mode 100644 tests/sv-comp/cfg/uncil/and_ambiguous_partition3.expected
 create mode 100644 tests/sv-comp/cfg/uncil/and_ambiguous_partition4.c
 create mode 100644 tests/sv-comp/cfg/uncil/and_ambiguous_partition4.expected

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..1e9d8abf5d
--- /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)
+  ▼
+┌──────────────────────────────────┐
+│                _                 │
+└──────────────────────────────────┘
+  │
+  │ 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..3923536a15
--- /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),true)
+  │                                   ▼
+  │                                 ┌──────────────────────────────────┐
+  │                                 │                _                 │
+  │                                 └──────────────────────────────────┘
+  │                                   │
+  │                                   │ Ret (Some 1, main)
+  │                                   ▼
+  │   Ret (Some 0, main)            ┌──────────────────────────────────┐
+  └───────────────────────────────▶ │                _                 │
+                                    └──────────────────────────────────┘
diff --git a/tests/sv-comp/dune.inc b/tests/sv-comp/dune.inc
index d06aba05b8..3ff8f5a872 100644
--- a/tests/sv-comp/dune.inc
+++ b/tests/sv-comp/dune.inc
@@ -814,6 +814,94 @@
   (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

From 1180f83e383a41d136200dd109f45898ca5ba87f Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 11 Sep 2025 13:40:52 +0300
Subject: [PATCH 66/73] Return all possible paths MyARG.partition_if_next

---
 src/arg/myARG.ml                              | 74 ++++++++++++-------
 .../uncil/and_ambiguous_partition1.expected   | 66 ++++++++---------
 .../uncil/and_ambiguous_partition4.expected   | 28 +++----
 3 files changed, 95 insertions(+), 73 deletions(-)

diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index a65aa4355f..580e1a0e75 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -278,18 +278,43 @@ struct
   let next_opt _ = None
 end
 
-let partition_if_next if_next_n =
+type path = (edge * node) list
+let cartesian_concat_paths (ps : path list) (qs : path list) : path list = List.concat (List.map (fun p -> List.map (fun q -> p @ q) qs) ps)
+let mk_edges (e : edge) (n : node) (paths : path list) : (edge * node * path) list = List.map (fun p -> (e, n, p)) paths
+let combine_and_make (e : edge) (n : node) (lhs : path list) (rhs : path list) : (edge * node * path) list = mk_edges e n (cartesian_concat_paths lhs rhs)
+
+let partition_if_next (if_next_n : (edge * node * (edge * node) list) list): exp * (node * path list) * (node * path list) =
   (* 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 exp =
+    match if_next_n with
+    | [] -> failwith "partition_if_next: empty"
+    | (Test (exp, _), _, _) :: xs ->
+      let all_tests_same_cond =
+        List.for_all
+          (function
+            | (Test (exp', _), _, _) -> Basetype.CilExp.equal exp exp'
+            | _ -> false)
+          xs
+      in
+      if all_tests_same_cond then exp
+      else failwith "partition_if_next: bad branches"
+    | _ -> failwith "partition_if_next: not Test edge"
+  in
+  let collapse_branch b =
+    let paths_for_b = List.filter (function
+        | (Test (_, b'), _, _) when b = b' -> true
+        | _ -> false)
+        if_next_n
+    in
+    match paths_for_b with
+    | [] -> failwith (if b then "partition_if_next: missing true-branch" else "partition_if_next: missing false-branch")
+    | (e, n, p) :: rest ->
+      let all_same_en = List.for_all (fun (e', n', _) -> Edge.equal e e' && Node.equal n n') paths_for_b in
+      if not all_same_en then failwith "partition_if_next: branch has differing (edge,node) pairs";
+      let paths = List.map (fun (_,_,p) -> p) paths_for_b in
+      (n, paths)
   in
-  (* assert (List.length if_next <= 2); *)
-  match test_next true, test_next false with
-  | (Test (e_true, true), if_true_next_n, if_true_next_p), (Test (e_false, false), if_false_next_n, if_false_next_p) when Basetype.CilExp.equal e_true e_false ->
-    (e_true, (if_true_next_n, if_true_next_p), (if_false_next_n, if_false_next_p))
-  | _, _ -> failwith "partition_if_next: bad branches"
+  (exp, collapse_branch true, collapse_branch false)
 
 module UnCilLogicIntra (Arg: SIntraOpt): SIntraOpt =
 struct
@@ -312,12 +337,11 @@ struct
           let (e2, (if_true_next_true_next_n, if_true_next_true_next_p), (if_true_next_false_next_n, if_true_next_false_next_p)) = 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, if_true_next_p @ if_true_next_true_next_p);
-              (* two different paths to same false node *)
-              (Test (exp, false), if_true_next_false_next_n, if_true_next_p @ if_true_next_false_next_p);
-              (Test (exp, false), if_false_next_n, if_false_next_p)
-            ]
+            let true_items = combine_and_make (Test (exp, true)) if_true_next_true_next_n if_true_next_p if_true_next_true_next_p in
+            (* two different path families to same false node *)
+            let false_from_true_items = combine_and_make (Test (exp, false)) if_true_next_false_next_n if_true_next_p if_true_next_false_next_p in
+            let false_from_false_items = mk_edges (Test (exp, false)) if_false_next_n if_false_next_p in
+            Some (true_items @ false_from_true_items @ false_from_false_items)
           else
             None
         (* || *)
@@ -326,12 +350,11 @@ struct
           let (e2, (if_false_next_true_next_n, if_false_next_true_next_p), (if_false_next_false_next_n, if_false_next_false_next_p)) = 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 [
-              (* two different paths to same true node *)
-              (Test (exp, true), if_true_next_n, if_true_next_p);
-              (Test (exp, true), if_false_next_true_next_n, if_false_next_p @ if_false_next_true_next_p);
-              (Test (exp, false), if_false_next_false_next_n, if_false_next_p @ if_false_next_false_next_p)
-            ]
+            (* two different path families to same true node *)
+            let true_from_true_items = mk_edges (Test (exp, true)) if_true_next_n if_true_next_p in
+            let true_from_false_items = combine_and_make (Test (exp, true)) if_false_next_true_next_n if_false_next_p if_false_next_true_next_p in
+            let false_from_false_items = combine_and_make (Test (exp, false)) if_false_next_false_next_n if_false_next_p if_false_next_false_next_p in
+            Some (true_from_true_items @ true_from_false_items @ false_from_false_items)
           else
             None
         | _, _ -> None
@@ -364,10 +387,9 @@ struct
         match Arg.next if_true_next_n, Arg.next if_false_next_n with
         | [(Assign (v_true, e_true), if_true_next_next_n, if_true_next_next_p)], [(Assign (v_false, e_false), if_false_next_next_n, if_false_next_next_p)] 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, if_true_next_p @ if_true_next_next_p);
-            (Assign (v_false, exp), if_false_next_next_n, if_false_next_p @ if_false_next_next_p)
-          ]
+          let assigns_true = combine_and_make (Assign (v_true, exp)) if_true_next_next_n if_true_next_p [if_true_next_next_p] in
+          let assigns_false = combine_and_make (Assign (v_false, exp)) if_false_next_next_n if_false_next_p [if_false_next_next_p] in
+          Some (assigns_true @ assigns_false)
         | _, _ -> None
       else
         None
diff --git a/tests/sv-comp/cfg/uncil/and_ambiguous_partition1.expected b/tests/sv-comp/cfg/uncil/and_ambiguous_partition1.expected
index 1e9d8abf5d..8c1a83b95a 100644
--- a/tests/sv-comp/cfg/uncil/and_ambiguous_partition1.expected
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous_partition1.expected
@@ -1,33 +1,33 @@
-┌──────────────────────────────────┐
-│                _                 │
-└──────────────────────────────────┘
-  │
-  │ Entry main
-  ▼
-┌──────────────────────────────────┐
-│                _                 │
-└──────────────────────────────────┘
-  │
-  │ Assign 'b = 0'
-  ▼
-┌──────────────────────────────────┐
-│                _                 │
-└──────────────────────────────────┘
-  │
-  │ Proc '__goblint_split_begin(a)'
-  ▼
-┌──────────────────────────────────┐
-│                _                 │
-└──────────────────────────────────┘
-  │
-  │ Test (a && (b && c),false)
-  ▼
-┌──────────────────────────────────┐
-│                _                 │
-└──────────────────────────────────┘
-  │
-  │ Ret (Some 0, main)
-  ▼
-┌──────────────────────────────────┐
-│                _                 │
-└──────────────────────────────────┘
+                                    ┌──────────────────────────────────┐
+                                    │                _                 │
+                                    └──────────────────────────────────┘
+                                      │
+                                      │ 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_partition4.expected b/tests/sv-comp/cfg/uncil/and_ambiguous_partition4.expected
index 3923536a15..01db9837f8 100644
--- a/tests/sv-comp/cfg/uncil/and_ambiguous_partition4.expected
+++ b/tests/sv-comp/cfg/uncil/and_ambiguous_partition4.expected
@@ -16,18 +16,18 @@
                                       │
                                       │ Proc '__goblint_split_begin(a)'
                                       ▼
-┌───┐  Test (a && (b && c),false)   ┌──────────────────────────────────┐
-│ _ │ ◀──────────────────────────── │                _                 │
-└───┘                               └──────────────────────────────────┘
-  │                                   │
-  │                                   │ Test (a && (b && c),true)
-  │                                   ▼
-  │                                 ┌──────────────────────────────────┐
-  │                                 │                _                 │
-  │                                 └──────────────────────────────────┘
-  │                                   │
-  │                                   │ Ret (Some 1, main)
-  │                                   ▼
-  │   Ret (Some 0, main)            ┌──────────────────────────────────┐
-  └───────────────────────────────▶ │                _                 │
+┌───┐  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)             │
+  └───────────────────────────────▶ │                _                 │ ◀───────────────────────────────┘
                                     └──────────────────────────────────┘

From b8b6041ff4809fb700f2ff770e022e7a76bb5152 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 1 Dec 2025 17:00:46 +0200
Subject: [PATCH 67/73] Simplify MyARG.partition_if_next by keeping triples
 paths with same edge and node grouped

---
 src/arg/myARG.ml | 60 ++++++++++++++++++++++--------------------------
 1 file changed, 28 insertions(+), 32 deletions(-)

diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index 580e1a0e75..a9b2f6ba27 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -257,15 +257,15 @@ type cfg_path = (MyCFG.edge * MyCFG.node) list
 
 module type SIntra =
 sig
-  val next: MyCFG.node -> (MyCFG.edge * MyCFG.node * cfg_path) list
-  (** @return Also the original CFG path corresponding to the step. *)
+  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 * cfg_path) list) option
-  (** @return Also the original CFG path corresponding to the step. *)
+  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 =
@@ -274,17 +274,14 @@ 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, [[(e, to_n)]])
   let next_opt _ = None
 end
 
-type path = (edge * node) list
-let cartesian_concat_paths (ps : path list) (qs : path list) : path list = List.concat (List.map (fun p -> List.map (fun q -> p @ q) qs) ps)
-let mk_edges (e : edge) (n : node) (paths : path list) : (edge * node * path) list = List.map (fun p -> (e, n, p)) paths
-let combine_and_make (e : edge) (n : node) (lhs : path list) (rhs : path list) : (edge * node * path) list = mk_edges e n (cartesian_concat_paths lhs rhs)
+let cartesian_concat_paths (ps : cfg_path list) (qs : cfg_path list) : cfg_path list = List.concat (List.map (fun p -> List.map (fun q -> p @ q) qs) ps)
 
-let partition_if_next (if_next_n : (edge * node * (edge * node) list) list): exp * (node * path list) * (node * path list) =
-  (* TODO: refactor, check extra edges for error *)
+let partition_if_next (if_next_n : (edge * node * cfg_path list) list): exp * (node * cfg_path list) * (node * cfg_path list) =
+  (* TODO: refactor *)
   let exp =
     match if_next_n with
     | [] -> failwith "partition_if_next: empty"
@@ -308,11 +305,10 @@ let partition_if_next (if_next_n : (edge * node * (edge * node) list) list): exp
     in
     match paths_for_b with
     | [] -> failwith (if b then "partition_if_next: missing true-branch" else "partition_if_next: missing false-branch")
-    | (e, n, p) :: rest ->
+    | (e, n, ps) :: rest -> (* TODO: rest is ignored, so this List.filter is almost a List.find, except it also checks if nodes are all same (for b) *)
       let all_same_en = List.for_all (fun (e', n', _) -> Edge.equal e e' && Node.equal n n') paths_for_b in
       if not all_same_en then failwith "partition_if_next: branch has differing (edge,node) pairs";
-      let paths = List.map (fun (_,_,p) -> p) paths_for_b in
-      (n, paths)
+      (n, ps)
   in
   (exp, collapse_branch true, collapse_branch false)
 
@@ -325,7 +321,7 @@ struct
 
   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_true_next_p), (if_false_next_n, if_false_next_p)) = 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? *)
@@ -334,27 +330,25 @@ 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_true_next_p), (if_true_next_false_next_n, if_true_next_false_next_p)) = partition_if_next (next if_true_next_n) in
+          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
-            let true_items = combine_and_make (Test (exp, true)) if_true_next_true_next_n if_true_next_p if_true_next_true_next_p in
-            (* two different path families to same false node *)
-            let false_from_true_items = combine_and_make (Test (exp, false)) if_true_next_false_next_n if_true_next_p if_true_next_false_next_p in
-            let false_from_false_items = mk_edges (Test (exp, false)) if_false_next_n if_false_next_p in
-            Some (true_items @ false_from_true_items @ false_from_false_items)
+            Some [
+              (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_true_next_p), (if_false_next_false_next_n, if_false_next_false_next_p)) = partition_if_next (next if_false_next_n) in
+          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
-            (* two different path families to same true node *)
-            let true_from_true_items = mk_edges (Test (exp, true)) if_true_next_n if_true_next_p in
-            let true_from_false_items = combine_and_make (Test (exp, true)) if_false_next_true_next_n if_false_next_p if_false_next_true_next_p in
-            let false_from_false_items = combine_and_make (Test (exp, false)) if_false_next_false_next_n if_false_next_p if_false_next_false_next_p in
-            Some (true_from_true_items @ true_from_false_items @ false_from_false_items)
+            Some [
+              (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
         | _, _ -> None
@@ -381,15 +375,16 @@ 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_true_next_p), (if_false_next_n, if_false_next_p)) = 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, if_true_next_next_p)], [(Assign (v_false, e_false), if_false_next_next_n, if_false_next_next_p)] 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
-          let assigns_true = combine_and_make (Assign (v_true, exp)) if_true_next_next_n if_true_next_p [if_true_next_next_p] in
-          let assigns_false = combine_and_make (Assign (v_false, exp)) if_false_next_next_n if_false_next_p [if_false_next_next_p] in
-          Some (assigns_true @ assigns_false)
+          Some [
+            (Assign (v_true, exp), if_true_next_next_n, cartesian_concat_paths if_true_next_ps if_true_next_next_ps);
+            (Assign (v_false, exp), if_false_next_next_n, cartesian_concat_paths if_false_next_ps if_false_next_next_ps)
+          ]
         | _, _ -> None
       else
         None
@@ -427,6 +422,7 @@ struct
     | Some next ->
       next
       |> 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)

From 6d6c124d5e1ecd53a2c15b5a09955f20d7132885 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 1 Dec 2025 17:11:55 +0200
Subject: [PATCH 68/73] Revert to old partition_if_next but with path lists

---
 src/arg/myARG.ml | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index a9b2f6ba27..dcde2298b2 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -280,6 +280,7 @@ end
 
 let cartesian_concat_paths (ps : cfg_path list) (qs : cfg_path list) : cfg_path list = List.concat (List.map (fun p -> List.map (fun q -> p @ q) qs) ps)
 
+(* TODO: remove *)
 let partition_if_next (if_next_n : (edge * node * cfg_path list) list): exp * (node * cfg_path list) * (node * cfg_path list) =
   (* TODO: refactor *)
   let exp =
@@ -312,6 +313,19 @@ let partition_if_next (if_next_n : (edge * node * cfg_path list) list): exp * (n
   in
   (exp, collapse_branch true, collapse_branch false)
 
+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
+  in
+  assert (List.length if_next_n <= 2);
+  match test_next true, test_next false with
+  | (Test (e_true, true), if_true_next_n, if_true_next_p), (Test (e_false, false), if_false_next_n, if_false_next_p) when Basetype.CilExp.equal e_true e_false ->
+    (e_true, (if_true_next_n, if_true_next_p), (if_false_next_n, if_false_next_p))
+  | _, _ -> failwith "partition_if_next: bad branches"
+
 module UnCilLogicIntra (Arg: SIntraOpt): SIntraOpt =
 struct
   open Cil

From 0db8feaf2964127321410213b0879c6814830b93 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Mon, 1 Dec 2025 17:16:19 +0200
Subject: [PATCH 69/73] Replace violation cram test

---
 .../witness/violation.t/callfpointer.c        |  21 ---
 tests/regression/witness/violation.t/nec11.c  |  34 +++++
 tests/regression/witness/violation.t/run.t    | 126 +++++++-----------
 3 files changed, 79 insertions(+), 102 deletions(-)
 delete mode 100644 tests/regression/witness/violation.t/callfpointer.c
 create mode 100644 tests/regression/witness/violation.t/nec11.c

diff --git a/tests/regression/witness/violation.t/callfpointer.c b/tests/regression/witness/violation.t/callfpointer.c
deleted file mode 100644
index b0d4f04bfb..0000000000
--- a/tests/regression/witness/violation.t/callfpointer.c
+++ /dev/null
@@ -1,21 +0,0 @@
-extern void abort(void);
-extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
-void reach_error() { __assert_fail("0", "callfpointer.c", 3, "reach_error"); }
-
-
-void f(void g(int)) {
- g(1);
-}
-
-void h(int i) {
- if(i==1) {
-  ERROR: {reach_error();abort();}
- } else {
-
- }
-}
-int main(void) {
- f(h);
-
- return 0;
-}
diff --git a/tests/regression/witness/violation.t/nec11.c b/tests/regression/witness/violation.t/nec11.c
new file mode 100644
index 0000000000..03c2f58728
--- /dev/null
+++ b/tests/regression/witness/violation.t/nec11.c
@@ -0,0 +1,34 @@
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "nec11.c", 3, "reach_error"); }
+
+void __VERIFIER_assert(int cond) {
+  if (!(cond)) {
+    ERROR: {reach_error();abort();}
+  }
+  return;
+}
+
+_Bool __VERIFIER_nondet_bool();
+
+int main(){
+   int a[5];
+   int len=0;
+   _Bool c=__VERIFIER_nondet_bool();
+   int i;
+
+
+   while(c){
+     
+      if (len==4)
+         len =0;
+      
+      a[len]=0;
+
+      len++;
+   }
+   __VERIFIER_assert(len==5);
+   return 1;
+
+   
+}
diff --git a/tests/regression/witness/violation.t/run.t b/tests/regression/witness/violation.t/run.t
index a17f4cd8c3..713f29b99e 100644
--- a/tests/regression/witness/violation.t/run.t
+++ b/tests/regression/witness/violation.t/run.t
@@ -1,72 +1,12 @@
-  $ goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )"} callfpointer.c --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --enable ana.wp  --set witness.yaml.entry-types[+] violation_sequence --enable witness.yaml.sv-comp-true-only --enable witness.invariant.other 
+  $ goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )"} nec11.c --enable exp.arg.enabled --enable ana.wp --set witness.yaml.entry-types[+] violation_sequence --enable witness.yaml.sv-comp-true-only --enable witness.invariant.other 
   [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
-  [Warning][Deadcode] Function 'main' does not return
-  [Warning][Deadcode] Function 'f' has dead code:
-    on line 8 (callfpointer.c:8-8)
-  [Warning][Deadcode] Function 'h' has dead code:
-    on line 16 (callfpointer.c:16-16)
-  [Warning][Deadcode] Function 'main' has dead code:
-    on line 20 (callfpointer.c:20-20)
-  [Warning][Deadcode] Logical lines of code (LLoC) summary:
-    live: 8
-    dead: 3
-    total lines: 11
-  [Warning][Deadcode][CWE-571] condition 'i == 1' is always true (callfpointer.c:11:5-11:9)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (nec11.c:28:7-28:12)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 16
+    dead: 0
+    total lines: 16
   SV-COMP result: unknown
 
-  $ graph-easy --as=boxart arg.dot
-  ┌──────────────────────┐
-  │          _           │
-  └──────────────────────┘
-    │
-    │ Entry main
-    ▼
-  ┌──────────────────────┐
-  │          _           │
-  └──────────────────────┘
-    │
-    │ InlineEntry '(& h)'
-    ▼
-  ┌──────────────────────┐
-  │          _           │
-  └──────────────────────┘
-    │
-    │ Entry f
-    ▼
-  ┌──────────────────────┐
-  │          _           │
-  └──────────────────────┘
-    │
-    │ InlineEntry '(1)'
-    ▼
-  ┌──────────────────────┐
-  │          _           │
-  └──────────────────────┘
-    │
-    │ Entry h
-    ▼
-  ┌──────────────────────┐
-  │          _           │
-  └──────────────────────┘
-    │
-    │ Test (i == 1,true)
-    ▼
-  ┌──────────────────────┐
-  │          _           │
-  └──────────────────────┘
-    │
-    │ InlineEntry '()'
-    ▼
-  ┌──────────────────────┐
-  │          _           │
-  └──────────────────────┘
-    │
-    │ Entry reach_error
-    ▼
-  ┌──────────────────────┐
-  │          _           │
-  └──────────────────────┘
-
   $ yamlWitnessStrip < witness.yml
   - entry_type: violation_sequence
     content:
@@ -74,9 +14,9 @@
       - waypoint:
           type: assumption
           location:
-            file_name: callfpointer.c
-            line: 18
-            column: 2
+            file_name: nec11.c
+            line: 16
+            column: 4
             function: main
           action: follow
           constraint:
@@ -86,10 +26,10 @@
       - waypoint:
           type: assumption
           location:
-            file_name: callfpointer.c
-            line: 7
-            column: 2
-            function: f
+            file_name: nec11.c
+            line: 17
+            column: 4
+            function: main
           action: follow
           constraint:
             value: "1"
@@ -98,10 +38,34 @@
       - waypoint:
           type: branching
           location:
-            file_name: callfpointer.c
-            line: 11
-            column: 2
-            function: h
+            file_name: nec11.c
+            line: 21
+            column: 4
+            function: main
+          action: follow
+          constraint:
+            value: "false"
+            format: c_expression
+    - segment:
+      - waypoint:
+          type: assumption
+          location:
+            file_name: nec11.c
+            line: 30
+            column: 4
+            function: main
+          action: follow
+          constraint:
+            value: "1"
+            format: c_expression
+    - segment:
+      - waypoint:
+          type: branching
+          location:
+            file_name: nec11.c
+            line: 6
+            column: 3
+            function: __VERIFIER_assert
           action: follow
           constraint:
             value: "true"
@@ -110,8 +74,8 @@
       - waypoint:
           type: target
           location:
-            file_name: callfpointer.c
-            line: 12
-            column: 11
-            function: h
+            file_name: nec11.c
+            line: 7
+            column: 13
+            function: __VERIFIER_assert
           action: follow

From bef86e2fc5a852ee03e6f31996dc6297c7c79cc1 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 1 Dec 2025 17:22:50 +0200
Subject: [PATCH 70/73] Refactor old partition_if_next to check for more errors

---
 src/arg/myARG.ml | 25 ++++++++++++++-----------
 1 file changed, 14 insertions(+), 11 deletions(-)

diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index dcde2298b2..40bb5df55d 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -313,18 +313,21 @@ let partition_if_next (if_next_n : (edge * node * cfg_path list) list): exp * (n
   in
   (exp, collapse_branch true, collapse_branch false)
 
-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 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_n <= 2);
-  match test_next true, test_next false with
-  | (Test (e_true, true), if_true_next_n, if_true_next_p), (Test (e_false, false), if_false_next_n, if_false_next_p) when Basetype.CilExp.equal e_true e_false ->
-    (e_true, (if_true_next_n, if_true_next_p), (if_false_next_n, if_false_next_p))
-  | _, _ -> 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

From eae4fb2d8efb381ff1e7be63c10dddd60acdbf96 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 1 Dec 2025 17:23:03 +0200
Subject: [PATCH 71/73] Remove Karoliine's partition_if_next

---
 src/arg/myARG.ml | 33 ---------------------------------
 1 file changed, 33 deletions(-)

diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index 40bb5df55d..c6739bf7ed 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -280,39 +280,6 @@ end
 
 let cartesian_concat_paths (ps : cfg_path list) (qs : cfg_path list) : cfg_path list = List.concat (List.map (fun p -> List.map (fun q -> p @ q) qs) ps)
 
-(* TODO: remove *)
-let partition_if_next (if_next_n : (edge * node * cfg_path list) list): exp * (node * cfg_path list) * (node * cfg_path list) =
-  (* TODO: refactor *)
-  let exp =
-    match if_next_n with
-    | [] -> failwith "partition_if_next: empty"
-    | (Test (exp, _), _, _) :: xs ->
-      let all_tests_same_cond =
-        List.for_all
-          (function
-            | (Test (exp', _), _, _) -> Basetype.CilExp.equal exp exp'
-            | _ -> false)
-          xs
-      in
-      if all_tests_same_cond then exp
-      else failwith "partition_if_next: bad branches"
-    | _ -> failwith "partition_if_next: not Test edge"
-  in
-  let collapse_branch b =
-    let paths_for_b = List.filter (function
-        | (Test (_, b'), _, _) when b = b' -> true
-        | _ -> false)
-        if_next_n
-    in
-    match paths_for_b with
-    | [] -> failwith (if b then "partition_if_next: missing true-branch" else "partition_if_next: missing false-branch")
-    | (e, n, ps) :: rest -> (* TODO: rest is ignored, so this List.filter is almost a List.find, except it also checks if nodes are all same (for b) *)
-      let all_same_en = List.for_all (fun (e', n', _) -> Edge.equal e e' && Node.equal n n') paths_for_b in
-      if not all_same_en then failwith "partition_if_next: branch has differing (edge,node) pairs";
-      (n, ps)
-  in
-  (exp, collapse_branch true, collapse_branch false)
-
 let partition_if_next if_next =
   let (if_next_trues, if_next_falses) = List.partition (function
       | (Test (_, b), _, _) -> b

From c630eae007f9f784880b2bb3c7fa8647052208f0 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 1 Dec 2025 17:24:52 +0200
Subject: [PATCH 72/73] Use List.concat_map in MyARG.cartesian_concat_paths

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

diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index c6739bf7ed..219bc46e03 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -278,7 +278,7 @@ struct
   let next_opt _ = None
 end
 
-let cartesian_concat_paths (ps : cfg_path list) (qs : cfg_path list) : cfg_path list = List.concat (List.map (fun p -> List.map (fun q -> p @ q) qs) ps)
+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

From 708edac281a198928f9a0b0f1acc46ea9c757b14 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 2 Dec 2025 15:54:29 +0200
Subject: [PATCH 73/73] Fix MyARG.UnCilTernaryIntra returning duplicate edge
 and node

Instead their paths should just be concatenated.
Introduced in b8b6041ff4809fb700f2ff770e022e7a76bb5152.
---
 src/arg/myARG.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml
index 219bc46e03..c41a442f10 100644
--- a/src/arg/myARG.ml
+++ b/src/arg/myARG.ml
@@ -366,8 +366,7 @@ struct
         | [(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, cartesian_concat_paths if_true_next_ps if_true_next_next_ps);
-            (Assign (v_false, exp), if_false_next_next_n, cartesian_concat_paths if_false_next_ps if_false_next_next_ps)
+            (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