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/Log_true-termination_true-no-overflow.c |
programSHA |
08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109 |
witnessName |
results-verified/2ls.2018-12-04_2244.logfiles/sv-comp19_prop-termination.Log_true-termination_true-no-overflow.c.files/witness.graphml |
witnessSHA |
44fc6f7ba7588f9775d7843a9681f6ce00eef0a4ea83b7a35bf56b53a140ee79 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/44fc6f7ba7588f9775d7843a9681f6ce00eef0a4ea83b7a35bf56b53a140ee79.json
Key |
Value |
architecture |
64bit |
creationtime |
2018-12-05T00:36 CET (sv-comp) |
producer |
2LS |
programfile |
../../sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c |
programhash |
2d80b45a01c32727728c3a89e06c1e9a4dc4868b |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(F end) ) |
witness-file |
witnessFileByHash/44fc6f7ba7588f9775d7843a9681f6ce00eef0a4ea83b7a35bf56b53a140ee79.graphml |
witness-sha256 |
44fc6f7ba7588f9775d7843a9681f6ce00eef0a4ea83b7a35bf56b53a140ee79 |
witness-size |
10029 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109, sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c).
Found 12 witnesses for program sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c, 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
fb1765c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T04:23:24Z |
|
42d296f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:53:18+01:00 |
|
ea6cb03 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
77b754d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
681 |
2023-12-20T03:55:49+01:00 |
ea6cb03 |
6110baf |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
641 |
2023-12-03T18:45:47+01:00 |
42d296f |
f21a20b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
106 |
2023-12-03T10:01:31+01:00 |
fb1765c |
37546fc |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
681 |
2023-11-30T08:19:53+01:00 |
|
88c1faa |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
692 |
2023-12-03T21:54:49+01:00 |
|
74ae8cb |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
681 |
2023-12-18T19:38:35+01:00 |
|
9f681a1 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
3 |
2023-12-01T02:08:01Z |
|
7771a3a |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
9 |
2023-11-30T21:17:19+01:00 |
|
ee1a375 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: 5d32cb67-3baa-4771-b541-cb19bfe0b2f4
creation_time: 2023-12-01T01:47:55Z
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/Log.c'''
task:
input_files:
- ../../sv-benchmarks/c/termination-restricted-15/Log.c
input_file_hashes:
../../sv-benchmarks/c/termination-restricted-15/Log.c: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
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/Log.c
file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
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/Log.c
file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
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/Log.c
file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
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/Log.c
file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
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/Log.c
file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
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/Log.c
file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
line: 13
column: 11
function: main
value: (4294967295LL + (long long )restmp) - (long long )xtmp >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/Log.c
file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
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/Log.c
file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
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/Log.c
file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
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/Log.c
file_hash: 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
line: 17
column: 15
function: main
value: (((0 <= xtmp && (long long )res + (long long )xtmp >= 0LL) && xtmp !=
-2) && ((xtmp != -4 && ((xtmp != -6 && ((xtmp != -8 && ((xtmp != -10 && ((xtmp
!= -12 && ((xtmp != -14 && ((xtmp != -16 && ((xtmp != -18 && ((xtmp != -20
&& ((xtmp != -22 && ((((((((((((((((((((12 <= restmp && xtmp <= 2147483623)
&& (-36LL + (long long )restmp) + (long long )x >= 0LL) && (-24LL + (long
long )x) + (long long )xtmp >= 0LL) && (-24LL + (long long )res) + (long long
)x >= 0LL) && (-12LL + (long long )res) + (long long )restmp >= 0LL) && (-12LL
+ (long long )restmp) + (long long )xtmp >= 0LL) && (-24LL + (long long )x)
- (long long )xtmp >= 0LL) && xtmp != -24) && restmp != 1) && restmp != 2)
&& restmp != 3) && restmp != 4) && restmp != 5) && restmp != 6) && restmp
!= 7) && restmp != 8) && restmp != 9) && restmp != 10) && restmp != 11) ||
(((((((((((xtmp <= 2147483625 && (-33LL + (long long )restmp) + (long long
)x >= 0LL) && (-22LL + (long long )x) + (long long )xtmp >= 0LL) && (-22LL
+ (long long )res) + (long long )x >= 0LL) && (-11LL + (long long )res) +
(long long )restmp >= 0LL) && (-11LL + (long long )restmp) + (long long )xtmp
>= 0LL) && (-11LL - (long long )restmp) + (long long )x >= 0LL) && (11LL -
(long long )restmp) + (long long )xtmp >= 0LL) && (22LL - (long long )x) +
(long long )xtmp >= 0LL) && (-22LL + (long long )x) - (long long )xtmp >=
0LL) && (11LL + (long long )res) - (long long )restmp >= 0LL) && restmp ==
11))) || (((((((((((xtmp <= 2147483627 && (-30LL + (long long )restmp) + (long
long )x >= 0LL) && (-20LL + (long long )x) + (long long )xtmp >= 0LL) && (-20LL
+ (long long )res) + (long long )x >= 0LL) && (-10LL + (long long )res) +
(long long )restmp >= 0LL) && (-10LL + (long long )restmp) + (long long )xtmp
>= 0LL) && (-10LL - (long long )restmp) + (long long )x >= 0LL) && (10LL -
(long long )restmp) + (long long )xtmp >= 0LL) && (20LL - (long long )x) +
(long long )xtmp >= 0LL) && (-20LL + (long long )x) - (long long )xtmp >=
0LL) && (10LL + (long long )res) - (long long )restmp >= 0LL) && restmp ==
10))) || (((((((((((xtmp <= 2147483629 && (-27LL + (long long )restmp) + (long
long )x >= 0LL) && (-18LL + (long long )x) + (long long )xtmp >= 0LL) && (-18LL
+ (long long )res) + (long long )x >= 0LL) && (-9LL + (long long )res) + (long
long )restmp >= 0LL) && (-9LL + (long long )restmp) + (long long )xtmp >=
0LL) && (-9LL - (long long )restmp) + (long long )x >= 0LL) && (9LL - (long
long )restmp) + (long long )xtmp >= 0LL) && (18LL - (long long )x) + (long
long )xtmp >= 0LL) && (-18LL + (long long )x) - (long long )xtmp >= 0LL) &&
(9LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 9))) ||
(((((((((((xtmp <= 2147483631 && (-24LL + (long long )restmp) + (long long
)x >= 0LL) && (-16LL + (long long )x) + (long long )xtmp >= 0LL) && (-16LL
+ (long long )res) + (long long )x >= 0LL) && (-8LL + (long long )res) + (long
long )restmp >= 0LL) && (-8LL + (long long )restmp) + (long long )xtmp >=
0LL) && (-8LL - (long long )restmp) + (long long )x >= 0LL) && (8LL - (long
long )restmp) + (long long )xtmp >= 0LL) && (16LL - (long long )x) + (long
long )xtmp >= 0LL) && (-16LL + (long long )x) - (long long )xtmp >= 0LL) &&
(8LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 8))) ||
(((((((((((xtmp <= 2147483633 && (-21LL + (long long )restmp) + (long long
)x >= 0LL) && (-14LL + (long long )x) + (long long )xtmp >= 0LL) && (-14LL
+ (long long )res) + (long long )x >= 0LL) && (-7LL + (long long )res) + (long
long )restmp >= 0LL) && (-7LL + (long long )restmp) + (long long )xtmp >=
0LL) && (-7LL - (long long )restmp) + (long long )x >= 0LL) && (7LL - (long
long )restmp) + (long long )xtmp >= 0LL) && (14LL - (long long )x) + (long
long )xtmp >= 0LL) && (-14LL + (long long )x) - (long long )xtmp >= 0LL) &&
(7LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 7))) ||
(((((((((((xtmp <= 2147483635 && (-18LL + (long long )restmp) + (long long
)x >= 0LL) && (-12LL + (long long )x) + (long long )xtmp >= 0LL) && (-12LL
+ (long long )res) + (long long )x >= 0LL) && (-6LL + (long long )res) + (long
long )restmp >= 0LL) && (-6LL + (long long )restmp) + (long long )xtmp >=
0LL) && (-6LL - (long long )restmp) + (long long )x >= 0LL) && (6LL - (long
long )restmp) + (long long )xtmp >= 0LL) && (12LL - (long long )x) + (long
long )xtmp >= 0LL) && (-12LL + (long long )x) - (long long )xtmp >= 0LL) &&
(6LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 6))) ||
(((((((((((xtmp <= 2147483637 && (-15LL + (long long )restmp) + (long long
)x >= 0LL) && (-10LL + (long long )x) + (long long )xtmp >= 0LL) && (-10LL
+ (long long )res) + (long long )x >= 0LL) && (-5LL + (long long )res) + (long
long )restmp >= 0LL) && (-5LL + (long long )restmp) + (long long )xtmp >=
0LL) && (-5LL - (long long )restmp) + (long long )x >= 0LL) && (5LL - (long
long )restmp) + (long long )xtmp >= 0LL) && (10LL - (long long )x) + (long
long )xtmp >= 0LL) && (-10LL + (long long )x) - (long long )xtmp >= 0LL) &&
(5LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 5))) ||
(((((((((((xtmp <= 2147483639 && (-12LL + (long long )restmp) + (long long
)x >= 0LL) && (-8LL + (long long )x) + (long long )xtmp >= 0LL) && (-8LL +
(long long )res) + (long long )x >= 0LL) && (-4LL + (long long )res) + (long
long )restmp >= 0LL) && (-4LL + (long long )restmp) + (long long )xtmp >=
0LL) && (-4LL - (long long )restmp) + (long long )x >= 0LL) && (4LL - (long
long )restmp) + (long long )xtmp >= 0LL) && (8LL - (long long )x) + (long
long )xtmp >= 0LL) && (-8LL + (long long )x) - (long long )xtmp >= 0LL) &&
(4LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 4))) ||
(((((((((((xtmp <= 2147483641 && (-9LL + (long long )restmp) + (long long
)x >= 0LL) && (-6LL + (long long )x) + (long long )xtmp >= 0LL) && (-6LL +
(long long )res) + (long long )x >= 0LL) && (-3LL + (long long )res) + (long
long )restmp >= 0LL) && (-3LL + (long long )restmp) + (long long )xtmp >=
0LL) && (-3LL - (long long )restmp) + (long long )x >= 0LL) && (3LL - (long
long )restmp) + (long long )xtmp >= 0LL) && (6LL - (long long )x) + (long
long )xtmp >= 0LL) && (-6LL + (long long )x) - (long long )xtmp >= 0LL) &&
(3LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 3))) ||
(((((((((((xtmp <= 2147483643 && (-6LL + (long long )restmp) + (long long
)x >= 0LL) && (-4LL + (long long )x) + (long long )xtmp >= 0LL) && (-4LL +
(long long )res) + (long long )x >= 0LL) && (-2LL + (long long )res) + (long
long )restmp >= 0LL) && (-2LL + (long long )restmp) + (long long )xtmp >=
0LL) && (-2LL - (long long )restmp) + (long long )x >= 0LL) && (2LL - (long
long )restmp) + (long long )xtmp >= 0LL) && (4LL - (long long )x) + (long
long )xtmp >= 0LL) && (-4LL + (long long )x) - (long long )xtmp >= 0LL) &&
(2LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 2))) ||
(((((((((((xtmp <= 2147483645 && (-3LL + (long long )restmp) + (long long
)x >= 0LL) && (-2LL + (long long )x) + (long long )xtmp >= 0LL) && (-2LL +
(long long )res) + (long long )x >= 0LL) && (-1LL + (long long )res) + (long
long )restmp >= 0LL) && (-1LL + (long long )restmp) + (long long )xtmp >=
0LL) && (-1LL - (long long )restmp) + (long long )x >= 0LL) && (1LL - (long
long )restmp) + (long long )xtmp >= 0LL) && (2LL - (long long )x) + (long
long )xtmp >= 0LL) && (-2LL + (long long )x) - (long long )xtmp >= 0LL) &&
(1LL + (long long )res) - (long long )restmp >= 0LL) && restmp == 1))) ||
(((((((((((((((2 <= xtmp && (-4LL + (long long )x) + (long long )xtmp >= 0LL)
&& (-2LL + (long long )res) + (long long )x >= 0LL) && (-2LL + (long long
)res) + (long long )xtmp >= 0LL) && (-2LL + (long long )restmp) + (long long
)x >= 0LL) && (-2LL + (long long )restmp) + (long long )xtmp >= 0LL) && (-2LL
- (long long )restmp) + (long long )x >= 0LL) && (-2LL - (long long )restmp)
+ (long long )xtmp >= 0LL) && (0LL - (long long )x) + (long long )xtmp >=
0LL) && (long long )res + (long long )restmp >= 0LL) && (long long )x - (long
long )xtmp >= 0LL) && (long long )res - (long long )restmp >= 0LL) && 0 ==
restmp) && x == xtmp) && restmp == 0) && xtmp != 0)
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
53 |
2023-12-01T05:25:02+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109, sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c).
Found 10 witnesses for program sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c, 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
9221177 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2022-12-09T09:51:36Z |
|
8c5aaab |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-22 |
4 |
2022-12-11T01:49:54+01:00 |
|
ea6cb03 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2022-12-12T11:00 CET (comp) |
|
e54f1b0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
692 |
2023-01-29T11:46:49+01:00 |
ea6cb03 |
6047057 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
681 |
2023-01-28T23:08:11+01:00 |
8c5aaab |
a15d610 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
120 |
2023-01-28T17:45:42+01:00 |
9221177 |
f021814 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
755 |
2022-12-10T19:31:18+01:00 |
|
e486b8a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-1715bd67dc+ |
755 |
2022-12-11T21:58:57+01:00 |
|
2205ced |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
766 |
2022-12-09T23:13:21+01:00 |
|
61b881c |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
9 |
2022-12-08T01:17:49+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109, sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c).
Found 1 witnesses for program sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c, 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
b0a63e0 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
9 |
2021-12-05T22:51:15+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109, sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c, 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109.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 (08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109, sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c, 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109.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 (08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109, sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c).
Found 1 witnesses for program sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c, 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
51f36d5 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Symbiotic |
1 |
2018-12-08T08:12 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109, sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c).
Found 2 witnesses for program sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c, 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
7216647 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 3.1 |
8 |
2017-12-01T16:42 CET (sv-comp) |
|
44fc6f7 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
10 |
2017-12-01T13:15 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109, sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-restricted-15/Log_true-termination_true-no-overflow.c, 08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/08d23a4fccc00925380f274033d6bce2f9ea0cd5a54ce734e93b963eb060b109.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |