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/b.09-no-inv_assume_true-termination_true-no-overflow.c |
programSHA |
b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575 |
witnessName |
results-verified/depthk.2017-12-01_1515.logfiles/sv-comp18.b.09-no-inv_assume_true-termination_true-no-overflow.c.files/witness.graphml |
witnessSHA |
b087f1357159a96a666aa25fd19c95181321948ab6a04f29ff40b41a314701fa |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/b087f1357159a96a666aa25fd19c95181321948ab6a04f29ff40b41a314701fa.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T17:08 CET (sv-comp) |
memoryModel |
precise |
producer |
ESBMC 3.1 |
program-sha256 |
b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_ee56dc93-55b7-4f06-96c4-94a10c75922f/sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c |
programhash |
cf6b3a74fd4060a216a178ad3d11a901c2ac840d |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/b087f1357159a96a666aa25fd19c95181321948ab6a04f29ff40b41a314701fa.graphml |
witness-sha256 |
b087f1357159a96a666aa25fd19c95181321948ab6a04f29ff40b41a314701fa |
witness-size |
6114 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575, sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c).
Found 10 witnesses for program sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c, b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
e3670cd |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T07:22:33Z |
|
a7430f8 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:16:36+01:00 |
|
3b6ed5e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
336fe4e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
686 |
2023-12-20T03:55:50+01:00 |
3b6ed5e |
3d36790 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
583 |
2023-12-03T18:48:25+01:00 |
a7430f8 |
13c3a7c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
134 |
2023-12-03T10:00:11+01:00 |
e3670cd |
d3c1b8f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
686 |
2023-11-30T08:14:36+01:00 |
|
b6e8856 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
643 |
2023-12-03T21:25:55+01:00 |
|
1976799 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
673 |
2023-12-18T22:21:56+01:00 |
|
bcc35c7 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: c05c28b2-9f6e-43ea-bdd4-e163a2d35ced
creation_time: 2023-12-01T02:09:53Z
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/b.09-no-inv_assume.c'''
task:
input_files:
- ../../sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume.c
input_file_hashes:
../../sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume.c: b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575
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/b.09-no-inv_assume.c
file_hash: b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575
line: 12
column: 15
function: main
value: y != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume.c
file_hash: b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575
line: 12
column: 15
function: main
value: (0 <= x && ((x != -1 && ((x != -2 && ((x != -3 && ((x != -4 && ((x !=
-5 && ((x != -6 && ((((((((7 <= y && 8 <= c) && x <= 2147483639) && (-15LL
+ (long long )c) + (long long )y >= 0LL) && (-8LL + (long long )c) + (long
long )x >= 0LL) && (-7LL + (long long )x) + (long long )y >= 0LL) && (-7LL
- (long long )x) + (long long )y >= 0LL) && x != -7) || ((((((((6 <= y &&
x <= 2147483640) && (-13LL + (long long )c) + (long long )y >= 0LL) && (-7LL
+ (long long )c) + (long long )x >= 0LL) && (-6LL + (long long )x) + (long
long )y >= 0LL) && (-6LL - (long long )x) + (long long )y >= 0LL) && (1LL
- (long long )c) + (long long )y >= 0LL) && (7LL - (long long )c) + (long
long )x >= 0LL) && c == 7))) || ((((((((5 <= y && x <= 2147483641) && (-11LL
+ (long long )c) + (long long )y >= 0LL) && (-6LL + (long long )c) + (long
long )x >= 0LL) && (-5LL + (long long )x) + (long long )y >= 0LL) && (-5LL
- (long long )x) + (long long )y >= 0LL) && (1LL - (long long )c) + (long
long )y >= 0LL) && (6LL - (long long )c) + (long long )x >= 0LL) && c == 6)))
|| ((((((((4 <= y && x <= 2147483642) && (-9LL + (long long )c) + (long long
)y >= 0LL) && (-5LL + (long long )c) + (long long )x >= 0LL) && (-4LL + (long
long )x) + (long long )y >= 0LL) && (-4LL - (long long )x) + (long long )y
>= 0LL) && (1LL - (long long )c) + (long long )y >= 0LL) && (5LL - (long long
)c) + (long long )x >= 0LL) && c == 5))) || ((((((((3 <= y && x <= 2147483643)
&& (-7LL + (long long )c) + (long long )y >= 0LL) && (-4LL + (long long )c)
+ (long long )x >= 0LL) && (-3LL + (long long )x) + (long long )y >= 0LL)
&& (-3LL - (long long )x) + (long long )y >= 0LL) && (1LL - (long long )c)
+ (long long )y >= 0LL) && (4LL - (long long )c) + (long long )x >= 0LL) &&
c == 4))) || ((((((((2 <= y && x <= 2147483644) && (-5LL + (long long )c)
+ (long long )y >= 0LL) && (-3LL + (long long )c) + (long long )x >= 0LL)
&& (-2LL + (long long )x) + (long long )y >= 0LL) && (-2LL - (long long )x)
+ (long long )y >= 0LL) && (1LL - (long long )c) + (long long )y >= 0LL) &&
(3LL - (long long )c) + (long long )x >= 0LL) && c == 3))) || ((((((((1 <=
y && x <= 2147483645) && (-3LL + (long long )c) + (long long )y >= 0LL) &&
(-2LL + (long long )c) + (long long )x >= 0LL) && (-1LL + (long long )x) +
(long long )y >= 0LL) && (-1LL - (long long )x) + (long long )y >= 0LL) &&
(1LL - (long long )c) + (long long )y >= 0LL) && (2LL - (long long )c) + (long
long )x >= 0LL) && c == 2))) || ((((((((1 <= y && x <= 2147483646) && (-2LL
+ (long long )c) + (long long )y >= 0LL) && (-1LL + (long long )c) + (long
long )x >= 0LL) && (-1LL + (long long )x) + (long long )y >= 0LL) && (0LL
- (long long )c) + (long long )y >= 0LL) && (0LL - (long long )x) + (long
long )y >= 0LL) && (1LL - (long long )c) + (long long )x >= 0LL) && c == 1)))
|| (((((((((1 <= x && 1 <= y) && (-2LL + (long long )x) + (long long )y >=
0LL) && (-1LL + (long long )c) + (long long )x >= 0LL) && (-1LL + (long long
)c) + (long long )y >= 0LL) && (-1LL - (long long )c) + (long long )x >= 0LL)
&& (-1LL - (long long )c) + (long long )y >= 0LL) && 0 == c) && c == 0) &&
x != 0)
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
564 |
2023-12-01T04:21:32+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575, sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c).
Found 10 witnesses for program sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c, b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
2ca6dce |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2022-12-09T13:14:57Z |
|
263ebac |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-22 |
4 |
2022-12-11T01:53:11+01:00 |
|
3b6ed5e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2022-12-12T11:02 CET (comp) |
|
61a8577 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
634 |
2023-01-29T11:46:48+01:00 |
3b6ed5e |
8903a56 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
621 |
2023-01-28T23:06:02+01:00 |
263ebac |
32a3e12 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
5 |
2023-01-28T18:50:45+01:00 |
8a08403 |
d68ec17 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
140 |
2023-01-28T17:47:18+01:00 |
2ca6dce |
4205b82 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
727 |
2022-12-10T20:13:14+01:00 |
|
75a07ea |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-1715bd67dc+ |
727 |
2022-12-12T01:53:43+01:00 |
|
8a08403 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
5 |
2022-12-10T04:10:11+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575, sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c, b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575.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 (b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575, sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c, b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575.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 (b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575, sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c, b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575.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 (b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575, sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c, b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575.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 (b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575, sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c).
Found 1 witnesses for program sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c, b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
b087f13 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 3.1 |
6 |
2017-12-01T17:08 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575, sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c, b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/b5b0de00a094cfc3c067192c4a42cb6740c5eeeb1cc4308b3b5e47b47532a575.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |