Witness Inspection

A description of this web service can be found in the CAV paper "Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses" (more material).

This link does not point to a witness, but below is a list of witnesses for the same program.

Available Results for the Program from Witness Store SV-COMP '24

Trying to find witnesses for program (45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84, sv-benchmarks/c/termination-crafted/NonTerminationSimple4_false-no-overflow.c).

Found 13 witnesses for program sv-benchmarks/c/termination-crafted/NonTerminationSimple4_false-no-overflow.c, 45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 844111e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T06:24:13Z
Download 7c161ef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:57:24+01:00
Download b134ebc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download 216c0db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-20T03:55:29+01:00 Download b134ebc
Download c1c1885 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-19T04:14:34+01:00 Download c81e14f
Download fbc403a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-04T01:42:50+01:00 Download c33be91
Download 672ae25 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-03T18:44:18+01:00 Download 7c161ef
Download 4c1affd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-03T10:02:39+01:00 Download 844111e
Download a3bafa4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-30T12:56:39+01:00 Download 1bb195f
Download 1bb195f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-30T06:48:57+01:00
Download c33be91 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 4 2023-12-04T00:57:45+01:00
Download c81e14f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2023-12-18T23:28:56+01:00
Download d6846f0 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 896b533b-3853-4d3f-884c-6a8f68647f5d creation_time: 2023-12-01T01:44:44Z producer: name: Goblint version: tags/svcomp24-0-gc2e9465a7 command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--sets'' ''ana.specification'' ''../../sv-benchmarks/c/properties/no-overflow.prp'' ''--sets'' ''exp.architecture'' ''64bit'' ''../../sv-benchmarks/c/termination-crafted/NonTerminationSimple4.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted/NonTerminationSimple4.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted/NonTerminationSimple4.c: 45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/NonTerminationSimple4.c file_hash: 45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84 line: 18 column: 12 function: main value: ((0 <= x && ((((((((((((((((((((y != -13 && ((y != -14 && ((y != -15 && ((y != -16 && ((((-12 <= y && y <= 2147483630) && (12LL + (long long )x) + (long long )y >= 0LL) && y != -17) || (((-11 <= y && y <= 2147483631) && (11LL + (long long )x) + (long long )y >= 0LL) && y != -12))) || ((((-10 <= y && y <= 2147483632) && (10LL + (long long )x) + (long long )y >= 0LL) && y != -12) && y != -11))) || (((((-9 <= y && y <= 2147483633) && (9LL + (long long )x) + (long long )y >= 0LL) && y != -12) && y != -11) && y != -10))) || ((((((-8 <= y && y <= 2147483634) && (8LL + (long long )x) + (long long )y >= 0LL) && y != -12) && y != -11) && y != -10) && y != -9))) || (((((((-7 <= y && y <= 2147483635) && (7LL + (long long )x) + (long long )y >= 0LL) && y != -12) && y != -11) && y != -10) && y != -9) && y != -8)) || (((((((-6 <= y && y <= 2147483636) && (6LL + (long long )x) + (long long )y >= 0LL) && y != -11) && y != -10) && y != -9) && y != -8) && y != -7)) || (((((((-5 <= y && y <= 2147483637) && (5LL + (long long )x) + (long long )y >= 0LL) && y != -10) && y != -9) && y != -8) && y != -7) && y != -6)) || (((((((-4 <= y && y <= 2147483638) && (4LL + (long long )x) + (long long )y >= 0LL) && y != -9) && y != -8) && y != -7) && y != -6) && y != -5)) || (((((((-3 <= y && y <= 2147483639) && (3LL + (long long )x) + (long long )y >= 0LL) && y != -8) && y != -7) && y != -6) && y != -5) && y != -4)) || (((((((-2 <= y && y <= 2147483640) && (2LL + (long long )x) + (long long )y >= 0LL) && y != -7) && y != -6) && y != -5) && y != -4) && y != -3)) || y <= 2147483622) || (((((((-1 <= y && y <= 2147483641) && (1LL + (long long )x) + (long long )y >= 0LL) && y != -6) && y != -5) && y != -4) && y != -3) && y != -2)) || (((((((-19 <= y && y <= 2147483623) && (19LL + (long long )x) + (long long )y >= 0LL) && y != -24) && y != -23) && y != -22) && y != -21) && y != -20)) || (((((((0 <= y && y <= 2147483642) && (long long )x + (long long )y >= 0LL) && y != -5) && y != -4) && y != -3) && y != -2) && y != -1)) || (((((((-18 <= y && y <= 2147483624) && (18LL + (long long )x) + (long long )y >= 0LL) && y != -23) && y != -22) && y != -21) && y != -20) && y != -19)) || ((((((1 <= y && y <= 2147483643) && (-1LL + (long long )x) + (long long )y >= 0LL) && y != -4) && y != -3) && y != -2) && y != -1)) || (((((((-17 <= y && y <= 2147483625) && (17LL + (long long )x) + (long long )y >= 0LL) && y != -22) && y != -21) && y != -20) && y != -19) && y != -18)) || (((((2 <= y && y <= 2147483644) && (-2LL + (long long )x) + (long long )y >= 0LL) && y != -3) && y != -2) && y != -1)) || (((((((-16 <= y && y <= 2147483626) && (16LL + (long long )x) + (long long )y >= 0LL) && y != -21) && y != -20) && y != -19) && y != -18) && y != -17)) || ((((3 <= y && y <= 2147483645) && (-3LL + (long long )x) + (long long )y >= 0LL) && y != -2) && y != -1)) || (((((((-15 <= y && y <= 2147483627) && (15LL + (long long )x) + (long long )y >= 0LL) && y != -20) && y != -19) && y != -18) && y != -17) && y != -16)) || (((4 <= y && y <= 2147483646) && (-4LL + (long long )x) + (long long )y >= 0LL) && y != -1)) || (((((((-14 <= y && y <= 2147483628) && (14LL + (long long )x) + (long long )y >= 0LL) && y != -19) && y != -18) && y != -17) && y != -16) && y != -15))) || (5 <= y && y != 0)) || ((((((((-13 <= y && 0 <= x) && y <= 2147483629) && (13LL + (long long )x) + (long long )y >= 0LL) && y != -18) && y != -17) && y != -16) && y != -15) && y != -14) format: c_expression correctness_witness CPAchecker 2.3 11 2023-12-01T04:41:39+01:00

Available Results for the Program from Witness Store SV-COMP '23

Trying to find witnesses for program (45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84, sv-benchmarks/c/termination-crafted/NonTerminationSimple4_false-no-overflow.c).

Found 12 witnesses for program sv-benchmarks/c/termination-crafted/NonTerminationSimple4_false-no-overflow.c, 45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 40f77c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T11:57:25Z
Download 09be290 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-11T01:53:29+01:00
Download b134ebc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T11:00 CET (comp)
Download d50f11c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T11:46:38+01:00 Download b134ebc
Download f5d4fcd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T03:01:57+01:00 Download 96e054c
Download 88b0148 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T23:06:23+01:00 Download 09be290
Download 49dc7c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T19:11:14+01:00 Download 71a8e1b
Download fa2f038 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T17:48:27+01:00 Download 40f77c6
Download c2502b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T11:52:16+01:00 Download b7e004c
Download b7e004c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2022-12-10T18:41:05+01:00
Download 96e054c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 4 2022-12-11T22:08:30+01:00
Download 71a8e1b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2022-12-09T23:50:17+01:00

Available Results for the Program from Witness Store SV-COMP '22

Trying to find witnesses for program (45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84, sv-benchmarks/c/termination-crafted/NonTerminationSimple4_false-no-overflow.c).

Found 6 witnesses for program sv-benchmarks/c/termination-crafted/NonTerminationSimple4_false-no-overflow.c, 45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 848b947 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.8 3 2021-12-13T20:33:12Z
Download dba1ca4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2021-12-06T13:39:30+01:00
Download 206240f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-14T00:09:25+01:00 Download 848b947
Download 48622b1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-05T18:57:19+01:00
Download 1706dda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 4 2021-12-08T19:16:56+01:00
Download be6c984 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 4 2021-12-09T12:19:55+01:00

Available Results for the Program from Witness Store SV-COMP '21

Trying to find witnesses for program (45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84, sv-benchmarks/c/termination-crafted/NonTerminationSimple4_false-no-overflow.c).

Found 5 witnesses for program sv-benchmarks/c/termination-crafted/NonTerminationSimple4_false-no-overflow.c, 45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 328f8f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.1 3 2020-12-06T23:51:29
Download 8c778ac Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) unknown_witness Goblint (svcomp21-0-g82e03b87) 3 2020-12-07T17:28:28
Download d6a8160 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-07T00:10:26+01:00 Download 328f8f3
Download f657398 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-05T14:24:01+01:00
Download 1edb30c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 4 2020-12-08T05:47:33+01:00

Available Results for the Program from Witness Store SV-COMP '20

Trying to find witnesses for program (45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84, sv-benchmarks/c/termination-crafted/NonTerminationSimple4_false-no-overflow.c).

Found 4 witnesses for program sv-benchmarks/c/termination-crafted/NonTerminationSimple4_false-no-overflow.c, 45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 9d32cf0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 4 2019-12-11T21:59:04+01:00 Download dcb0898
Download c2fd83f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 4 2019-12-03T08:09:46+01:00 Download e52ebaa
Download e52ebaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 4 2019-11-29T16:52:12+01:00
Download dcb0898 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 4 2019-12-01T18:19:47+01:00

Available Results for the Program from Witness Store SV-COMP '19

Trying to find witnesses for program (45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84, sv-benchmarks/c/termination-crafted/NonTerminationSimple4_false-no-overflow.c).

Found 4 witnesses for program sv-benchmarks/c/termination-crafted/NonTerminationSimple4_false-no-overflow.c, 45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 43b9cdd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness Symbiotic 2 2018-12-08T01:17 CET (sv-comp)
Download 26b55fd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-07T14:21:07+01:00
Download 78b10c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-08T23:46:00+01:00 Download 43b9cdd
Download 2762785 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T05:04:45+01:00

Available Results for the Program from Witness Store SV-COMP '18

Trying to find witnesses for program (45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84, sv-benchmarks/c/termination-crafted/NonTerminationSimple4_false-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/NonTerminationSimple4_false-no-overflow.c, 45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness

Available Results for the Program from Witness Store SV-COMP '17

Trying to find witnesses for program (45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84, sv-benchmarks/c/termination-crafted/NonTerminationSimple4_false-no-overflow.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/NonTerminationSimple4_false-no-overflow.c, 45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness