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 01/17] 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 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 02/17] 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 03/17] 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 04/17] 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 05/17] 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 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 06/17] 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 07/17] 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 08/17] 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 09/17] 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 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 10/17] 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 11/17] 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 12/17] 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 13/17] 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 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 14/17] 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 15/17] 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 16/17] 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 17/17] 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