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-restricted-15/DivMinus2_true-termination_true-no-overflow.c |
programSHA |
804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de |
witnessName |
results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-termination.DivMinus2_true-termination_true-no-overflow.c.files/witness.graphml |
witnessSHA |
2cdeaf4abf578e644a2e20a6edc7074b8d4433351249565ea4719b7e673261b7 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/2cdeaf4abf578e644a2e20a6edc7074b8d4433351249565ea4719b7e673261b7.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-06T04:38:09.192687 |
producer |
DepthK v3.0 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_8f2b98d7-1db0-4450-bd4e-0631e4fe20b4/sv-benchmarks/c/termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c |
programhash |
4113f10404cd50c48db8fb998633f502f8a0b01a |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/2cdeaf4abf578e644a2e20a6edc7074b8d4433351249565ea4719b7e673261b7.graphml |
witness-sha256 |
2cdeaf4abf578e644a2e20a6edc7074b8d4433351249565ea4719b7e673261b7 |
witness-size |
3496 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de, sv-benchmarks/c/termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c).
Found 13 witnesses for program sv-benchmarks/c/termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c, 804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
c5dce7a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T06:41:39Z |
|
03c2e07 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:23:37+01:00 |
|
93dcacb |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:36 CET (comp) |
|
7a7443d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-20T03:55:54+01:00 |
93dcacb |
e027e4e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-19T04:54:25+01:00 |
8ea4180 |
fa9e4f4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-04T01:46:40+01:00 |
ecd4f1f |
4188050 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-03T18:45:26+01:00 |
03c2e07 |
bc50389 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-03T10:00:54+01:00 |
c5dce7a |
432617f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-30T11:58:31+01:00 |
68170b9 |
68170b9 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-30T05:40:34+01:00 |
|
ecd4f1f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
6 |
2023-12-04T00:50:42+01:00 |
|
8ea4180 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
6 |
2023-12-18T17:20:24+01:00 |
|
4c0f5da |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: 857c5a96-d7a8-4a4a-97bf-1845c11ee94f
creation_time: 2023-12-01T00:56:33Z
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-restricted-15/DivMinus2.c'''
task:
input_files:
- ../../sv-benchmarks/c/termination-restricted-15/DivMinus2.c
input_file_hashes:
../../sv-benchmarks/c/termination-restricted-15/DivMinus2.c: 804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de
data_model: LP64
language: C
specification: CHECK( init(main()), LTL(G ! overflow) )
content:
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/DivMinus2.c
file_hash: 804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de
line: 16
column: 15
function: main
value: 0 <= res
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/DivMinus2.c
file_hash: 804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de
line: 16
column: 15
function: main
value: 1 <= y
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/DivMinus2.c
file_hash: 804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de
line: 16
column: 15
function: main
value: (long long )x - (long long )ytmp >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/DivMinus2.c
file_hash: 804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de
line: 16
column: 15
function: main
value: y != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/DivMinus2.c
file_hash: 804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de
line: 16
column: 15
function: main
value: (((((((0 <= x && 0 <= ytmp) && (long long )x + (long long )ytmp >= 0LL)
&& (long long )res + (long long )x >= 0LL) && (long long )res + (long long
)ytmp >= 0LL) && x != -1) && ytmp != -1) && (((x != -2 && ytmp != -2) && (((x
!= -3 && ytmp != -3) && (((x != -4 && ytmp != -4) && (((x != -5 && ytmp !=
-5) && ((((((((x <= 2147483641 && ytmp <= 2147483641) && (-6LL + (long long
)x) + (long long )y >= 0LL) && (-6LL + (long long )y) + (long long )ytmp >=
0LL) && (-6LL + (long long )res) + (long long )y >= 0LL) && (-6LL + (long
long )y) - (long long )ytmp >= 0LL) && x != -6) && ytmp != -6) || (((((((x
<= 2147483642 && ytmp <= 2147483642) && (-5LL + (long long )x) + (long long
)y >= 0LL) && (-5LL + (long long )y) + (long long )ytmp >= 0LL) && (-5LL +
(long long )res) + (long long )y >= 0LL) && (5LL - (long long )y) + (long
long )ytmp >= 0LL) && (-5LL + (long long )y) - (long long )ytmp >= 0LL) &&
(5LL + (long long )x) - (long long )y >= 0LL))) || (((((((x <= 2147483643
&& ytmp <= 2147483643) && (-4LL + (long long )x) + (long long )y >= 0LL) &&
(-4LL + (long long )y) + (long long )ytmp >= 0LL) && (-4LL + (long long )res)
+ (long long )y >= 0LL) && (4LL - (long long )y) + (long long )ytmp >= 0LL)
&& (-4LL + (long long )y) - (long long )ytmp >= 0LL) && (4LL + (long long
)x) - (long long )y >= 0LL))) || (((((((x <= 2147483644 && ytmp <= 2147483644)
&& (-3LL + (long long )x) + (long long )y >= 0LL) && (-3LL + (long long )y)
+ (long long )ytmp >= 0LL) && (-3LL + (long long )res) + (long long )y >=
0LL) && (3LL - (long long )y) + (long long )ytmp >= 0LL) && (-3LL + (long
long )y) - (long long )ytmp >= 0LL) && (3LL + (long long )x) - (long long
)y >= 0LL))) || (((((((x <= 2147483645 && ytmp <= 2147483645) && (-2LL + (long
long )x) + (long long )y >= 0LL) && (-2LL + (long long )y) + (long long )ytmp
>= 0LL) && (-2LL + (long long )res) + (long long )y >= 0LL) && (2LL - (long
long )y) + (long long )ytmp >= 0LL) && (-2LL + (long long )y) - (long long
)ytmp >= 0LL) && (2LL + (long long )x) - (long long )y >= 0LL))) || (((((((x
<= 2147483646 && ytmp <= 2147483646) && (-1LL + (long long )x) + (long long
)y >= 0LL) && (-1LL + (long long )y) + (long long )ytmp >= 0LL) && (-1LL +
(long long )res) + (long long )y >= 0LL) && (1LL - (long long )y) + (long
long )ytmp >= 0LL) && (-1LL + (long long )y) - (long long )ytmp >= 0LL) &&
(1LL + (long long )x) - (long long )y >= 0LL))) || (((((((((((1 <= ytmp &&
(-2LL + (long long )x) + (long long )y >= 0LL) && (-2LL + (long long )x) +
(long long )ytmp >= 0LL) && (-2LL + (long long )y) + (long long )ytmp >= 0LL)
&& (-1LL + (long long )res) + (long long )x >= 0LL) && (-1LL + (long long
)res) + (long long )y >= 0LL) && (-1LL + (long long )res) + (long long )ytmp
>= 0LL) && (0LL - (long long )y) + (long long )ytmp >= 0LL) && (long long
)x - (long long )y >= 0LL) && (long long )y - (long long )ytmp >= 0LL) &&
y == ytmp) && ytmp != 0)
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/DivMinus2.c
file_hash: 804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de
line: 14
column: 11
function: main
value: 0 <= res
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/DivMinus2.c
file_hash: 804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de
line: 14
column: 11
function: main
value: (2147483648LL + (long long )res) + (long long )ytmp >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/DivMinus2.c
file_hash: 804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de
line: 14
column: 11
function: main
value: (2147483647LL + (long long )res) - (long long )ytmp >= 0LL
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
13 |
2023-12-01T04:17:36+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de, sv-benchmarks/c/termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c).
Found 12 witnesses for program sv-benchmarks/c/termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c, 804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
fe25a75 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2022-12-09T12:35:34Z |
|
e48bae6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-22 |
4 |
2022-12-11T01:45:56+01:00 |
|
93dcacb |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2022-12-12T11:02 CET (comp) |
|
c5584d1 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
6 |
2023-01-29T11:46:55+01:00 |
93dcacb |
3f83570 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
6 |
2023-01-29T03:22:38+01:00 |
0950dd0 |
ce1090c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
6 |
2023-01-28T23:07:55+01:00 |
e48bae6 |
b170ef7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
6 |
2023-01-28T18:42:28+01:00 |
6b7614d |
2428019 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
6 |
2023-01-28T17:48:09+01:00 |
fe25a75 |
88aa09b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
6 |
2023-01-28T11:38:07+01:00 |
2f8bb2d |
2f8bb2d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
6 |
2022-12-10T17:38:29+01:00 |
|
0950dd0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-1715bd67dc+ |
6 |
2022-12-11T21:25:40+01:00 |
|
6b7614d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
6 |
2022-12-10T04:41:16+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de, sv-benchmarks/c/termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c, 804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de.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 '21
Trying to find witnesses for program (804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de, sv-benchmarks/c/termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c, 804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de.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 '20
Trying to find witnesses for program (804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de, sv-benchmarks/c/termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c, 804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de.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 '19
Trying to find witnesses for program (804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de, sv-benchmarks/c/termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c, 804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de.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 '18
Trying to find witnesses for program (804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de, sv-benchmarks/c/termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c).
Found 1 witnesses for program sv-benchmarks/c/termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c, 804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
3c1d631 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 3.1 |
11 |
2017-12-01T15:30 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de, sv-benchmarks/c/termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c, 804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/804e8d646f3136915195a4e5e9f5153cc3c1cd2abf96df3f09c683a14a27e4de.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |