Unconfirmed invariants in SV-COMP 2026

[karoliineh]

During the SV-COMP 2026 pre-runs, several invariants remain unconfirmed.
Because these invariants are not self-validated, and no other tool validates them either, our corresponding verification results are not confirmed.

Overall: correct-unconfirmed true 146

C.no-overflow.Main correct-unconfirmed true 48

• 8 unknown
• 40 ERROR (witness error)

Some of the smaller examples:

[Warning][Witness] invariant unconfirmed: c == ch (../../sv-benchmarks/c/termination-dietlibc/strchr-1.i:509:3)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 1
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1

------------

[Success][Witness] invariant confirmed: 0 == l (../../sv-benchmarks/c/termination-dietlibc/strrchr_short.i:510:3)
[Warning][Witness] invariant unconfirmed: c == ch (../../sv-benchmarks/c/termination-dietlibc/strrchr_short.i:510:3)
[Success][Witness] invariant confirmed: l == 0 (../../sv-benchmarks/c/termination-dietlibc/strrchr_short.i:510:3)
[Info][Witness] witness validation summary:
  confirmed: 2
  unconfirmed: 1
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0

C.unreach-call.Recursive correct-unconfirmed true 2

• 2 ERROR (witness error) (all having "couldn't locate invariant")

Issues with invariant paths: "couldn't locate invariant"

./goblint --conf conf/svcomp26-validate.json --witness.yaml.unassume ../../results-verified/goblint.2025-11-01_23-27-41.files/SV-COMP26_no-overflow/strrchr_short.yml/witness.yml --witness.yaml.validate ../../results-verified/goblint.2025-11-01_23-27-41.files/SV-COMP26_no-overflow/strrchr_short.yml/witness.yml --sets ana.specification ../../sv-benchmarks/c/properties/no-overflow.prp --sets exp.architecture 64bit ../../sv-benchmarks/c/termination-dietlibc/strrchr_short.i

...
[Warning][Witness] couldn't locate invariant: 2147483647LL >= (long long )sum + (long long )n (/home/cwd/sv-benchmarks/c/verifythis/prefixsum_rec.c:45:5)
[Warning][Witness] couldn't locate invariant: (long long )sum + 2147483647LL >= (long long )n (/home/cwd/sv-benchmarks/c/verifythis/prefixsum_rec.c:45:5)
[Warning][Witness] couldn't locate invariant: sum == 0 (/home/cwd/sv-benchmarks/c/verifythis/prefixsum_rec.c:45:5)

where run path ../../sv-benchmarks/c/termination-dietlibc/strrchr_short.i and invariant path /home/cwd/sv-benchmarks/c/verifythis/prefixsum_rec.c do not match.

C.unreach-call.ProductLines correct-unconfirmed true 4

• 4 ERROR (witness error) (all having "couldn't locate invariant")

C.unreach-call.Loops correct-unconfirmed true 6

• 3 unknown (unconfirmed invariants pretty large)
• 3 ERROR (witness error) (all having "couldn't locate invariant")

C.unreach-call.SoftwareSystems-DeviceDriversLinux64 correct-unconfirmed true 85

• 6 unknown
• 79 ERROR (witness error) (all having "couldn't locate invariant")

Examples

[Warning][Witness] invariant unconfirmed: __tmp == __tmpl (../../sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko.cil.out.i:5299:3)
[Warning][Witness] invariant unconfirmed: __tmp == __tmpl___0 (../../sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko.cil.out.i:5299:3)
[Warning][Witness] invariant unconfirmed: __tmp == & zone->free_sectors (../../sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko.cil.out.i:5299:3)
[Warning][Witness] invariant unconfirmed: __kfifo == & __tmp->__annonCompField39.kfifo (../../sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko.cil.out.i:5299:3)
[Warning][Witness] invariant unconfirmed: ftl == erase.priv (../../sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko.cil.out.i:4603:7)
[Warning][Witness] invariant unconfirmed: mtd == erase.mtd (../../sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko.cil.out.i:4603:7)

------------

[Error][Witness] CIL couldn't parse invariant: (__len == 1UL || __len == 2UL) || __len == 13UL (../../sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko.cil.out.i:6365:7)

------------

[Error][Witness] CIL couldn't parse invariant: hdr_len == 10UL || hdr_len == 12UL (../../sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko.cil.out.i:13562:3)

------------

[Error][Witness] CIL couldn't parse invariant: ((bw == 5000U || bw == 6000U) || bw == 7000U) || bw == 8000U (../../sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--media--dvb--frontends--dib3000mc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i:4581:3)

------------

[Error][Witness] CIL couldn't parse invariant: dm_digtable.FAHighThresh == 0U || dm_digtable.FAHighThresh == 1000U (../../sv-benchmarks/c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--staging--rtl8192e--rtl8192e--r8192e_pci.ko-ldv_main7_sequence_infinite_withcheck_stateful.cil.out.i:29980:3)

C.unreach-call.SoftwareSystems-Other correct-unconfirmed true 1

comment in #1722:

The following still needs fixing:
[Warning][Witness] invariant unconfirmed: applet_opts == (char const *)"lwmcL" (../../sv-benchmarks/c/busybox-1.22.0/wc-2.i:2458:3)

It's from one of the 7/31 tasks from SoftwareSystems-Other-ReachSafety that we are able to verify, and this one (high-value) result is unconfirmed due to this one invariant.

[sim642]

I think some/many of the "couldn't locate invariant" may be fixed with --disable pre.transform-paths. SV-COMP 2026 conf now uses preprocessing on .c files and we have some special logic for changing paths in preprocessor location pragmas.
I'll do a validator run to see if it makes a difference.