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-numeric/twisted_true-termination_true-no-overflow.c |
programSHA |
1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272 |
witnessName |
results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-termination.twisted_true-termination_true-no-overflow.c.files/witness.graphml |
witnessSHA |
9f1b6d7f08f6b4d9bf28232244096136324d507edaec4f9dcd0f777c5606261d |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/9f1b6d7f08f6b4d9bf28232244096136324d507edaec4f9dcd0f777c5606261d.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-06T06:19:19.729501 |
producer |
DepthK v3.0 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_bbfcf577-51b1-4168-8da3-879f81c6e2c9/sv-benchmarks/c/termination-numeric/twisted_true-termination_true-no-overflow.c |
programhash |
56facc094037ea8aa088ee9a4faafddcfe652feb |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/9f1b6d7f08f6b4d9bf28232244096136324d507edaec4f9dcd0f777c5606261d.graphml |
witness-sha256 |
9f1b6d7f08f6b4d9bf28232244096136324d507edaec4f9dcd0f777c5606261d |
witness-size |
3488 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272, sv-benchmarks/c/termination-numeric/twisted_true-termination_true-no-overflow.c).
Found 13 witnesses for program sv-benchmarks/c/termination-numeric/twisted_true-termination_true-no-overflow.c, 1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
4c289c1 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T07:07:35Z |
|
a2656f4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:44:11+01:00 |
|
26f8e38 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
db98dd0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-20T03:55:46+01:00 |
26f8e38 |
6ec1969 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-19T03:12:22+01:00 |
29e48b6 |
b9a6bfe |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-04T01:28:30+01:00 |
3eaf57c |
e7e9d10 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-03T18:46:05+01:00 |
a2656f4 |
f07dfee |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-03T10:01:41+01:00 |
4c289c1 |
5f12498 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-30T13:00:36+01:00 |
e17bc82 |
e17bc82 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-30T09:37:35+01:00 |
|
3eaf57c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
6 |
2023-12-03T21:20:11+01:00 |
|
29e48b6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
6 |
2023-12-19T01:36:09+01:00 |
|
4591915 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: b99d3f12-b4b5-4244-8736-7623695b04fc
creation_time: 2023-12-01T01:13:26Z
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-numeric/twisted.c'''
task:
input_files:
- ../../sv-benchmarks/c/termination-numeric/twisted.c
input_file_hashes:
../../sv-benchmarks/c/termination-numeric/twisted.c: 1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272
data_model: LP64
language: C
specification: CHECK( init(main()), LTL(G ! overflow) )
content:
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-numeric/twisted.c
file_hash: 1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272
line: 6
column: 11
function: f
value: (((((((((0LL - (long long )i) + (long long )j >= 0LL && (long long )i
+ (long long )j >= 0LL) && (0LL - (long long )i) - (long long )j >= 0LL) &&
(long long )i - (long long )j >= 0LL) && 0 == i) && 0 == j) && i == 0) &&
i == j) && j == 0) || ((0 <= i && 0 <= j) && (-1LL + (long long )i) + (long
long )j >= 0LL)
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-numeric/twisted.c
file_hash: 1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272
line: 13
column: 11
function: f
value: 0 <= i
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-numeric/twisted.c
file_hash: 1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272
line: 13
column: 11
function: f
value: 0 <= j
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-numeric/twisted.c
file_hash: 1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272
line: 13
column: 11
function: f
value: ((long long )i + (long long )j >= 0LL && (long long )i - (long long )k
>= 0LL) || (-1LL + (long long )i) + (long long )j >= 0LL
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-01T04:15:59+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272, sv-benchmarks/c/termination-numeric/twisted_true-termination_true-no-overflow.c).
Found 12 witnesses for program sv-benchmarks/c/termination-numeric/twisted_true-termination_true-no-overflow.c, 1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
b465fb7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2022-12-09T13:35:09Z |
|
09c70e3 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-22 |
4 |
2022-12-11T01:42:52+01:00 |
|
26f8e38 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2022-12-12T10:59 CET (comp) |
|
61cabc4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
6 |
2023-01-29T11:46:46+01:00 |
26f8e38 |
64db887 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
6 |
2023-01-29T02:51:01+01:00 |
3f123c2 |
972ccb0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
6 |
2023-01-28T23:06:40+01:00 |
09c70e3 |
daaf9dc |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
6 |
2023-01-28T19:15:12+01:00 |
2f1e45d |
b599cc0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
6 |
2023-01-28T17:46:54+01:00 |
b465fb7 |
e8df406 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
6 |
2023-01-28T11:43:56+01:00 |
aa9d13e |
aa9d13e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
6 |
2022-12-10T18:32:10+01:00 |
|
3f123c2 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-1715bd67dc+ |
6 |
2022-12-12T02:39:09+01:00 |
|
2f1e45d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
6 |
2022-12-10T04:41:33+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272, sv-benchmarks/c/termination-numeric/twisted_true-termination_true-no-overflow.c).
Found 10 witnesses for program sv-benchmarks/c/termination-numeric/twisted_true-termination_true-no-overflow.c, 1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
8bce539 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.2.8 |
3 |
2021-12-13T21:46:23Z |
|
f0459ed |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-22 |
4 |
2021-12-06T14:16:37+01:00 |
|
ded6bd0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
6 |
2021-12-09T16:12:34+01:00 |
17786f1 |
e20c949 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
6 |
2021-12-08T21:42:21+01:00 |
a423607 |
eec0f45 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
6 |
2021-12-06T15:02:53+01:00 |
f0459ed |
7567aa9 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
6 |
2021-12-05T20:27:42+01:00 |
30f0656 |
30f0656 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
6 |
2021-12-05T18:26:56+01:00 |
|
a423607 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-fe6f522dd3+ |
6 |
2021-12-08T20:32:40+01:00 |
|
17786f1 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-eda176372c+ |
6 |
2021-12-09T11:14:05+01:00 |
|
469f60a |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2021-12-10T18:28:37 |
|
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272, sv-benchmarks/c/termination-numeric/twisted_true-termination_true-no-overflow.c).
Found 8 witnesses for program sv-benchmarks/c/termination-numeric/twisted_true-termination_true-no-overflow.c, 1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
e89669c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.2.1 |
3 |
2020-12-06T23:36:32 |
|
2bbebfb |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
unknown_witness |
Goblint (svcomp21-0-g82e03b87) |
3 |
2020-12-07T16:59:03 |
|
685e9e5 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0 |
6 |
2020-12-08T06:34:55+01:00 |
5c0e561 |
b210f7c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0 |
6 |
2020-12-06T14:14:26+01:00 |
09279af |
09279af |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0 |
6 |
2020-12-05T15:19:45+01:00 |
|
5c0e561 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-eda176372c+ |
6 |
2020-12-07T23:25:52+01:00 |
|
d5bf0a6 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-11T19:10:32 |
|
3e684e1 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
2 |
2020-12-08T19:34:21 |
|
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272, sv-benchmarks/c/termination-numeric/twisted_true-termination_true-no-overflow.c).
Found 2 witnesses for program sv-benchmarks/c/termination-numeric/twisted_true-termination_true-no-overflow.c, 1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
a5200f2 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 1.9 |
6 |
2019-11-30T03:55:46+01:00 |
|
67ab51b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ |
6 |
2019-11-30T22:31:18+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272, sv-benchmarks/c/termination-numeric/twisted_true-termination_true-no-overflow.c).
Found 3 witnesses for program sv-benchmarks/c/termination-numeric/twisted_true-termination_true-no-overflow.c, 1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
33584ae |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
SMACK 1.9.3 |
3 |
2018-12-08T02:10:56 |
|
4743d38 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
6 |
2018-12-07T05:33:50+01:00 |
|
ce32043 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
6 |
2018-12-05T23:19:05+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272, sv-benchmarks/c/termination-numeric/twisted_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-numeric/twisted_true-termination_true-no-overflow.c, 1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272.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 (1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272, sv-benchmarks/c/termination-numeric/twisted_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-numeric/twisted_true-termination_true-no-overflow.c, 1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/1b68c797f7da07f29717590596e5fa31674f85e16d7b32a9335da92aff43a272.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |