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/LogAG_true-termination_true-no-overflow.c |
programSHA |
68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f |
witnessName |
results-verified/depthk.2018-12-05_0936.logfiles/sv-comp19_prop-termination.LogAG_true-termination_true-no-overflow.c.files/witness.graphml |
witnessSHA |
09e533d6f98bcbece24691fc02f6a6d2b9831b489bd0337006a386a5f64bfef4 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/09e533d6f98bcbece24691fc02f6a6d2b9831b489bd0337006a386a5f64bfef4.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-05T14:06:50.050396 |
producer |
DepthK v3.0 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_b406e044-d59f-49df-9865-48a68a769e20/sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c |
programhash |
81a46fe8790e1f522cb67a9c253c8a7e6828f982 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/09e533d6f98bcbece24691fc02f6a6d2b9831b489bd0337006a386a5f64bfef4.graphml |
witness-sha256 |
09e533d6f98bcbece24691fc02f6a6d2b9831b489bd0337006a386a5f64bfef4 |
witness-size |
3492 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f, sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c).
Found 11 witnesses for program sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c, 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
5afc074 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T04:09:45Z |
|
7e0b795 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:55:46+01:00 |
|
6d36477 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
849e2a8 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
1498 |
2023-12-20T03:55:43+01:00 |
6d36477 |
3cbc125 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
112 |
2023-12-03T18:44:07+01:00 |
7e0b795 |
11865d6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-03T10:01:14+01:00 |
5afc074 |
c660132 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
592 |
2023-11-30T05:07:38+01:00 |
|
e5ee225 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
1633 |
2023-12-03T22:04:47+01:00 |
|
dac613f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
1717 |
2023-12-18T18:09:26+01:00 |
|
125b296 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
3 |
2023-11-30T22:38:00Z |
|
b3cefe9 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: 846120f0-7fc9-474f-ac31-a44d167ec659
creation_time: 2023-12-01T00:57:23Z
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/LogAG.c'''
task:
input_files:
- ../../sv-benchmarks/c/termination-restricted-15/LogAG.c
input_file_hashes:
../../sv-benchmarks/c/termination-restricted-15/LogAG.c: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
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/LogAG.c
file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
line: 17
column: 15
function: main
value: 0 <= xtmp
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/LogAG.c
file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
line: 17
column: 15
function: main
value: 0 <= res
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/LogAG.c
file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
line: 17
column: 15
function: main
value: 2 <= x
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/LogAG.c
file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
line: 17
column: 15
function: main
value: (long long )res + (long long )xtmp >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/LogAG.c
file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
line: 17
column: 15
function: main
value: x != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/LogAG.c
file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
line: 17
column: 15
function: main
value: xtmp != -2
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/LogAG.c
file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
line: 17
column: 15
function: main
value: (xtmp != -4 && ((xtmp != -6 && ((xtmp != -8 && ((xtmp != -10 && ((xtmp
!= -12 && ((xtmp != -14 && ((xtmp != -16 && ((xtmp != -18 && ((xtmp != -20
&& ((xtmp != -22 && ((xtmp != -24 && ((((((((((((((((((((12 <= restmp && xtmp
<= 2147483621) && (-38LL + (long long )restmp) + (long long )x >= 0LL) &&
(-26LL + (long long )x) + (long long )xtmp >= 0LL) && (-26LL + (long long
)res) + (long long )x >= 0LL) && (-12LL + (long long )res) + (long long )restmp
>= 0LL) && (-12LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-26LL
+ (long long )x) - (long long )xtmp >= 0LL) && xtmp != -26) && restmp != 1)
&& restmp != 2) && restmp != 3) && restmp != 4) && restmp != 5) && restmp
!= 6) && restmp != 7) && restmp != 8) && restmp != 9) && restmp != 10) &&
restmp != 11) || (((((((((((xtmp <= 2147483623 && (-35LL + (long long )restmp)
+ (long long )x >= 0LL) && (-24LL + (long long )x) + (long long )xtmp >= 0LL)
&& (-24LL + (long long )res) + (long long )x >= 0LL) && (-11LL + (long long
)res) + (long long )restmp >= 0LL) && (-11LL + (long long )restmp) + (long
long )xtmp >= 0LL) && (-13LL - (long long )restmp) + (long long )x >= 0LL)
&& (11LL - (long long )restmp) + (long long )xtmp >= 0LL) && (24LL - (long
long )x) + (long long )xtmp >= 0LL) && (-24LL + (long long )x) - (long long
)xtmp >= 0LL) && (11LL + (long long )res) - (long long )restmp >= 0LL) &&
restmp == 11))) || (((((((((((xtmp <= 2147483625 && (-32LL + (long long )restmp)
+ (long long )x >= 0LL) && (-22LL + (long long )x) + (long long )xtmp >= 0LL)
&& (-22LL + (long long )res) + (long long )x >= 0LL) && (-10LL + (long long
)res) + (long long )restmp >= 0LL) && (-10LL + (long long )restmp) + (long
long )xtmp >= 0LL) && (-12LL - (long long )restmp) + (long long )x >= 0LL)
&& (10LL - (long long )restmp) + (long long )xtmp >= 0LL) && (22LL - (long
long )x) + (long long )xtmp >= 0LL) && (-22LL + (long long )x) - (long long
)xtmp >= 0LL) && (10LL + (long long )res) - (long long )restmp >= 0LL) &&
restmp == 10))) || (((((((((((xtmp <= 2147483627 && (-29LL + (long long )restmp)
+ (long long )x >= 0LL) && (-20LL + (long long )x) + (long long )xtmp >= 0LL)
&& (-20LL + (long long )res) + (long long )x >= 0LL) && (-9LL + (long long
)res) + (long long )restmp >= 0LL) && (-9LL + (long long )restmp) + (long
long )xtmp >= 0LL) && (-11LL - (long long )restmp) + (long long )x >= 0LL)
&& (9LL - (long long )restmp) + (long long )xtmp >= 0LL) && (20LL - (long
long )x) + (long long )xtmp >= 0LL) && (-20LL + (long long )x) - (long long
)xtmp >= 0LL) && (9LL + (long long )res) - (long long )restmp >= 0LL) && restmp
== 9))) || (((((((((((xtmp <= 2147483629 && (-26LL + (long long )restmp) +
(long long )x >= 0LL) && (-18LL + (long long )x) + (long long )xtmp >= 0LL)
&& (-18LL + (long long )res) + (long long )x >= 0LL) && (-8LL + (long long
)res) + (long long )restmp >= 0LL) && (-8LL + (long long )restmp) + (long
long )xtmp >= 0LL) && (-10LL - (long long )restmp) + (long long )x >= 0LL)
&& (8LL - (long long )restmp) + (long long )xtmp >= 0LL) && (18LL - (long
long )x) + (long long )xtmp >= 0LL) && (-18LL + (long long )x) - (long long
)xtmp >= 0LL) && (8LL + (long long )res) - (long long )restmp >= 0LL) && restmp
== 8))) || (((((((((((xtmp <= 2147483631 && (-23LL + (long long )restmp) +
(long long )x >= 0LL) && (-16LL + (long long )x) + (long long )xtmp >= 0LL)
&& (-16LL + (long long )res) + (long long )x >= 0LL) && (-7LL + (long long
)res) + (long long )restmp >= 0LL) && (-7LL + (long long )restmp) + (long
long )xtmp >= 0LL) && (-9LL - (long long )restmp) + (long long )x >= 0LL)
&& (7LL - (long long )restmp) + (long long )xtmp >= 0LL) && (16LL - (long
long )x) + (long long )xtmp >= 0LL) && (-16LL + (long long )x) - (long long
)xtmp >= 0LL) && (7LL + (long long )res) - (long long )restmp >= 0LL) && restmp
== 7))) || (((((((((((xtmp <= 2147483633 && (-20LL + (long long )restmp) +
(long long )x >= 0LL) && (-14LL + (long long )x) + (long long )xtmp >= 0LL)
&& (-14LL + (long long )res) + (long long )x >= 0LL) && (-6LL + (long long
)res) + (long long )restmp >= 0LL) && (-6LL + (long long )restmp) + (long
long )xtmp >= 0LL) && (-8LL - (long long )restmp) + (long long )x >= 0LL)
&& (6LL - (long long )restmp) + (long long )xtmp >= 0LL) && (14LL - (long
long )x) + (long long )xtmp >= 0LL) && (-14LL + (long long )x) - (long long
)xtmp >= 0LL) && (6LL + (long long )res) - (long long )restmp >= 0LL) && restmp
== 6))) || (((((((((((xtmp <= 2147483635 && (-17LL + (long long )restmp) +
(long long )x >= 0LL) && (-12LL + (long long )x) + (long long )xtmp >= 0LL)
&& (-12LL + (long long )res) + (long long )x >= 0LL) && (-5LL + (long long
)res) + (long long )restmp >= 0LL) && (-5LL + (long long )restmp) + (long
long )xtmp >= 0LL) && (-7LL - (long long )restmp) + (long long )x >= 0LL)
&& (5LL - (long long )restmp) + (long long )xtmp >= 0LL) && (12LL - (long
long )x) + (long long )xtmp >= 0LL) && (-12LL + (long long )x) - (long long
)xtmp >= 0LL) && (5LL + (long long )res) - (long long )restmp >= 0LL) && restmp
== 5))) || (((((((((((xtmp <= 2147483637 && (-14LL + (long long )restmp) +
(long long )x >= 0LL) && (-10LL + (long long )x) + (long long )xtmp >= 0LL)
&& (-10LL + (long long )res) + (long long )x >= 0LL) && (-4LL + (long long
)res) + (long long )restmp >= 0LL) && (-4LL + (long long )restmp) + (long
long )xtmp >= 0LL) && (-6LL - (long long )restmp) + (long long )x >= 0LL)
&& (4LL - (long long )restmp) + (long long )xtmp >= 0LL) && (10LL - (long
long )x) + (long long )xtmp >= 0LL) && (-10LL + (long long )x) - (long long
)xtmp >= 0LL) && (4LL + (long long )res) - (long long )restmp >= 0LL) && restmp
== 4))) || (((((((((((xtmp <= 2147483639 && (-11LL + (long long )restmp) +
(long long )x >= 0LL) && (-8LL + (long long )x) + (long long )xtmp >= 0LL)
&& (-8LL + (long long )res) + (long long )x >= 0LL) && (-3LL + (long long
)res) + (long long )restmp >= 0LL) && (-3LL + (long long )restmp) + (long
long )xtmp >= 0LL) && (-5LL - (long long )restmp) + (long long )x >= 0LL)
&& (3LL - (long long )restmp) + (long long )xtmp >= 0LL) && (8LL - (long long
)x) + (long long )xtmp >= 0LL) && (-8LL + (long long )x) - (long long )xtmp
>= 0LL) && (3LL + (long long )res) - (long long )restmp >= 0LL) && restmp
== 3))) || (((((((((((xtmp <= 2147483641 && (-8LL + (long long )restmp) +
(long long )x >= 0LL) && (-6LL + (long long )x) + (long long )xtmp >= 0LL)
&& (-6LL + (long long )res) + (long long )x >= 0LL) && (-2LL + (long long
)res) + (long long )restmp >= 0LL) && (-2LL + (long long )restmp) + (long
long )xtmp >= 0LL) && (-4LL - (long long )restmp) + (long long )x >= 0LL)
&& (2LL - (long long )restmp) + (long long )xtmp >= 0LL) && (6LL - (long long
)x) + (long long )xtmp >= 0LL) && (-6LL + (long long )x) - (long long )xtmp
>= 0LL) && (2LL + (long long )res) - (long long )restmp >= 0LL) && restmp
== 2))) || (((((((((((xtmp <= 2147483643 && (-5LL + (long long )restmp) +
(long long )x >= 0LL) && (-4LL + (long long )x) + (long long )xtmp >= 0LL)
&& (-4LL + (long long )res) + (long long )x >= 0LL) && (-1LL + (long long
)res) + (long long )restmp >= 0LL) && (-1LL + (long long )restmp) + (long
long )xtmp >= 0LL) && (-3LL - (long long )restmp) + (long long )x >= 0LL)
&& (1LL - (long long )restmp) + (long long )xtmp >= 0LL) && (4LL - (long long
)x) + (long long )xtmp >= 0LL) && (-4LL + (long long )x) - (long long )xtmp
>= 0LL) && (1LL + (long long )res) - (long long )restmp >= 0LL) && restmp
== 1))) || ((((((((((((xtmp <= 2147483645 && (-2LL + (long long )x) + (long
long )xtmp >= 0LL) && (-2LL + (long long )res) + (long long )x >= 0LL) &&
(-2LL + (long long )restmp) + (long long )x >= 0LL) && (-2LL - (long long
)restmp) + (long long )x >= 0LL) && (0LL - (long long )restmp) + (long long
)xtmp >= 0LL) && (2LL - (long long )x) + (long long )xtmp >= 0LL) && (long
long )res + (long long )restmp >= 0LL) && (long long )restmp + (long long
)xtmp >= 0LL) && (-2LL + (long long )x) - (long long )xtmp >= 0LL) && (long
long )res - (long long )restmp >= 0LL) && 0 == restmp) && restmp == 0)
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/LogAG.c
file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
line: 13
column: 11
function: main
value: 0 <= res
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/LogAG.c
file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
line: 13
column: 11
function: main
value: (2147483648LL + (long long )res) + (long long )xtmp >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/LogAG.c
file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
line: 13
column: 11
function: main
value: (2147483648LL + (long long )res) + (long long )restmp >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/LogAG.c
file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
line: 13
column: 11
function: main
value: (4294967296LL + (long long )restmp) + (long long )xtmp >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/LogAG.c
file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
line: 13
column: 11
function: main
value: (2147483647LL + (long long )res) - (long long )xtmp >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/LogAG.c
file_hash: 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
line: 13
column: 11
function: main
value: (4294967295LL + (long long )restmp) - (long long )xtmp >= 0LL
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
1121 |
2023-12-01T04:20:12+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f, sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c).
Found 11 witnesses for program sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c, 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
c8493d3 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2022-12-09T13:41:05Z |
|
a4c8fa0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.2 |
4 |
2023-01-28T17:59:17+01:00 |
0a7abf7 |
f8a2de6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.2 |
4 |
2023-01-28T11:39:32+01:00 |
0cbf16a |
80fbd4a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-22 |
4 |
2022-12-11T01:49:44+01:00 |
|
6d36477 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2022-12-12T10:59 CET (comp) |
|
0cc9ac4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
6 |
2023-01-29T11:46:41+01:00 |
6d36477 |
9df9ca4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
1498 |
2023-01-28T23:05:34+01:00 |
80fbd4a |
9fb4d88 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
191 |
2023-01-28T17:46:55+01:00 |
c8493d3 |
0cbf16a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
6 |
2022-12-10T16:56:17+01:00 |
|
7882b7b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-1715bd67dc+ |
1803 |
2022-12-12T02:46:25+01:00 |
|
0a7abf7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
6 |
2022-12-10T03:28:50+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f, sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c, 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f.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 (68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f, sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c, 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f.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 (68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f, sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c, 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f.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 (68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f, sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c).
Found 1 witnesses for program sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c, 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
3a72c0b |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
1 |
2018-12-08T08:56 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f, sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c).
Found 1 witnesses for program sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c, 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
b2282b0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 3.1 |
8 |
2017-12-01T18:47 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f, sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/LogAG_true-termination_true-no-overflow.c, 68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/68bdf78f6f996480ccfcf11b22cc3b7892db15596cae3edf06123d71c4506b1f.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |