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).
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 |
844111e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T06:24:13Z | ||
7c161ef | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:57:24+01:00 | ||
b134ebc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2023-12-20T03:37 CET (comp) | ||
216c0db | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-20T03:55:29+01:00 | b134ebc | |
c1c1885 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-19T04:14:34+01:00 | c81e14f | |
fbc403a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-04T01:42:50+01:00 | c33be91 | |
672ae25 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-03T18:44:18+01:00 | 7c161ef | |
4c1affd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-12-03T10:02:39+01:00 | 844111e | |
a3bafa4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-30T12:56:39+01:00 | 1bb195f | |
1bb195f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 4 | 2023-11-30T06:48:57+01:00 | ||
c33be91 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 4 | 2023-12-04T00:57:45+01:00 | ||
c81e14f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2023-12-18T23:28:56+01:00 | ||
d6846f0 | Inspect | - 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 |
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 |
40f77c6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T11:57:25Z | ||
09be290 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-11T01:53:29+01:00 | ||
b134ebc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2022-12-12T11:00 CET (comp) | ||
d50f11c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T11:46:38+01:00 | b134ebc | |
f5d4fcd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-29T03:01:57+01:00 | 96e054c | |
88b0148 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T23:06:23+01:00 | 09be290 | |
49dc7c7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T19:11:14+01:00 | 71a8e1b | |
fa2f038 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T17:48:27+01:00 | 40f77c6 | |
c2502b9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2023-01-28T11:52:16+01:00 | b7e004c | |
b7e004c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 4 | 2022-12-10T18:41:05+01:00 | ||
96e054c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 4 | 2022-12-11T22:08:30+01:00 | ||
71a8e1b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2022-12-09T23:50:17+01:00 |
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 |
848b947 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.2.8 | 3 | 2021-12-13T20:33:12Z | ||
dba1ca4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2021-12-06T13:39:30+01:00 | ||
206240f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-14T00:09:25+01:00 | 848b947 | |
48622b1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 4 | 2021-12-05T18:57:19+01:00 | ||
1706dda | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 4 | 2021-12-08T19:16:56+01:00 | ||
be6c984 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 4 | 2021-12-09T12:19:55+01:00 |
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 |
328f8f3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.2.1 | 3 | 2020-12-06T23:51:29 | ||
8c778ac | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | unknown_witness | Goblint (svcomp21-0-g82e03b87) | 3 | 2020-12-07T17:28:28 | ||
d6a8160 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-07T00:10:26+01:00 | 328f8f3 | |
f657398 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 4 | 2020-12-05T14:24:01+01:00 | ||
1edb30c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-eda176372c+ | 4 | 2020-12-08T05:47:33+01:00 |
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 |
9d32cf0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 4 | 2019-12-11T21:59:04+01:00 | dcb0898 | |
c2fd83f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 4 | 2019-12-03T08:09:46+01:00 | e52ebaa | |
e52ebaa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.9 | 4 | 2019-11-29T16:52:12+01:00 | ||
dcb0898 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 4 | 2019-12-01T18:19:47+01:00 |
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 |
43b9cdd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 2 | 2018-12-08T01:17 CET (sv-comp) | ||
26b55fd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 4 | 2018-12-07T14:21:07+01:00 | ||
78b10c9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T23:46:00+01:00 | 43b9cdd | |
2762785 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T05:04:45+01:00 |
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 |
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 |