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).
View and Validate the Witness
Input Given to this Service about the Witness (URL Query)
Key |
Value |
programName |
sv-benchmarks/c/termination-crafted/NonTerminationSimple4_false-no-overflow.c |
programSHA |
45cf92b0c6fea336569aa3c590b09eca22523fff4b1b234a5534ea2e1e74fe84 |
witnessName |
results-verified/map2check.2018-12-06_1220.logfiles/sv-comp19_prop-nooverflow.NonTerminationSimple4_false-no-overflow.c.files/witness.graphml |
witnessSHA |
b42c82922d085838cdc4aaf85dbe8a9299ad6ea415bb2fd8aff5cd165356dbd8 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/b42c82922d085838cdc4aaf85dbe8a9299ad6ea415bb2fd8aff5cd165356dbd8.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-06T12:36 CET (sv-comp) |
producer |
Map2Check |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_2309ff06-78fe-4eda-b6de-74f9e120a8a3/bin-2019/map2check/../../sv-benchmarks/c/termination-crafted/NonTerminationSimple4_false-no-overflow.c |
programhash |
3b4115924a616d2c9563d1567db185569a877e67 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! overflow) ) |
witness-file |
witnessFileByHash/b42c82922d085838cdc4aaf85dbe8a9299ad6ea415bb2fd8aff5cd165356dbd8.graphml |
witness-sha256 |
b42c82922d085838cdc4aaf85dbe8a9299ad6ea415bb2fd8aff5cd165356dbd8 |
witness-size |
2749 |
witness-type |
violation_witness |
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 |
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 |
|
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 |
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 |
|
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 |
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 |
|
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 |
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 |
|
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 |
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 |
|
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 |
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 |
|
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 |