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-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c |
programSHA |
9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135 |
witnessName |
results-verified/2ls.2017-12-01_1141.logfiles/sv-comp18.Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c.files/witness.graphml |
witnessSHA |
8b3f650b765bceff9bc1f1afc48607b7b1c84b1949df326c1a3888cfb0a24ae9 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/8b3f650b765bceff9bc1f1afc48607b7b1c84b1949df326c1a3888cfb0a24ae9.json
Key |
Value |
architecture |
64bit |
creationtime |
2017-12-01T12:51 CET (sv-comp) |
producer |
2LS |
program-sha256 |
9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135 |
programfile |
../../sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c |
programhash |
222b9e0025989dbea1cdc61cba66ae29f96b0141 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(F end) ) |
witness-file |
witnessFileByHash/8b3f650b765bceff9bc1f1afc48607b7b1c84b1949df326c1a3888cfb0a24ae9.graphml |
witness-sha256 |
8b3f650b765bceff9bc1f1afc48607b7b1c84b1949df326c1a3888cfb0a24ae9 |
witness-size |
10776 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135, sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c).
Found 11 witnesses for program sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c, 9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
c59bb9c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T08:05:52Z |
|
d61680e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:57:53+01:00 |
|
6249c15 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
3044536 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
2173 |
2023-12-20T03:55:52+01:00 |
6249c15 |
a2dd93a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
1270 |
2023-12-03T18:48:03+01:00 |
d61680e |
44614ac |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
348 |
2023-12-03T09:58:14+01:00 |
c59bb9c |
f857e1f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
2016 |
2023-11-30T09:29:46+01:00 |
|
03a228c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
2068 |
2023-12-04T00:39:01+01:00 |
|
1fa6634 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
2227 |
2023-12-18T19:07:13+01:00 |
|
815917d |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
10 |
2023-11-30T22:17:55+01:00 |
|
62ac80f |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: d46bf88d-02cf-4647-8b53-507c468e8b25
creation_time: 2023-12-01T01:53:03Z
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-crafted-lit/Avery-FLOPS2006-Table1.c'''
task:
input_files:
- ../../sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1.c
input_file_hashes:
../../sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1.c: 9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135
data_model: LP64
language: C
specification: CHECK( init(main()), LTL(G ! overflow) )
content:
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1.c
file_hash: 9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135
line: 25
column: 12
function: main
value: 1 <= x
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1.c
file_hash: 9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135
line: 25
column: 12
function: main
value: (-1LL + (long long )i) + (long long )z >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1.c
file_hash: 9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135
line: 25
column: 12
function: main
value: x != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1.c
file_hash: 9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135
line: 25
column: 12
function: main
value: y != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1.c
file_hash: 9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135
line: 25
column: 12
function: main
value: ((((((((((((1 <= y && (-2LL + (long long )x) + (long long )y >= 0LL)
&& (((((((((((0 <= z && z <= 2147483646) && (-2LL + (long long )i) + (long
long )x >= 0LL) && (-2LL + (long long )i) + (long long )y >= 0LL) && (-1LL
+ (long long )x) + (long long )z >= 0LL) && (-1LL + (long long )y) + (long
long )z >= 0LL) && (0LL - (long long )i) + (long long )x >= 0LL) && (0LL -
(long long )i) + (long long )y >= 0LL) && (1LL - (long long )i) + (long long
)z >= 0LL) && i == 1) && z != -1) || ((((((((1 <= z && (-2LL + (long long
)x) + (long long )z >= 0LL) && (-2LL + (long long )y) + (long long )z >= 0LL)
&& (-1LL + (long long )i) + (long long )x >= 0LL) && (-1LL + (long long )i)
+ (long long )y >= 0LL) && (-1LL - (long long )i) + (long long )x >= 0LL)
&& (-1LL - (long long )i) + (long long )y >= 0LL) && (-1LL - (long long )i)
+ (long long )z >= 0LL) && i == 0))) || (((((((12 <= y && 12 <= i) && z <=
2147483635) && (-24LL + (long long )i) + (long long )y >= 0LL) && (-13LL +
(long long )x) + (long long )y >= 0LL) && (-13LL + (long long )i) + (long
long )x >= 0LL) && (-1LL + (long long )y) + (long long )z >= 0LL) && (0LL
- (long long )i) + (long long )y >= 0LL)) || ((((((((((((-10 <= z && 11 <=
y) && z <= 2147483636) && (-22LL + (long long )i) + (long long )y >= 0LL)
&& (-12LL + (long long )x) + (long long )y >= 0LL) && (-12LL + (long long
)i) + (long long )x >= 0LL) && (-1LL + (long long )y) + (long long )z >= 0LL)
&& (9LL + (long long )x) + (long long )z >= 0LL) && (0LL - (long long )i)
+ (long long )y >= 0LL) && (10LL - (long long )i) + (long long )x >= 0LL)
&& (21LL - (long long )i) + (long long )z >= 0LL) && i == 11) && z != -11))
|| ((((((((((((-9 <= z && 10 <= y) && z <= 2147483637) && (-20LL + (long long
)i) + (long long )y >= 0LL) && (-11LL + (long long )x) + (long long )y >=
0LL) && (-11LL + (long long )i) + (long long )x >= 0LL) && (-1LL + (long long
)y) + (long long )z >= 0LL) && (8LL + (long long )x) + (long long )z >= 0LL)
&& (0LL - (long long )i) + (long long )y >= 0LL) && (9LL - (long long )i)
+ (long long )x >= 0LL) && (19LL - (long long )i) + (long long )z >= 0LL)
&& i == 10) && z != -10)) || ((((((((((((-8 <= z && 9 <= y) && z <= 2147483638)
&& (-18LL + (long long )i) + (long long )y >= 0LL) && (-10LL + (long long
)x) + (long long )y >= 0LL) && (-10LL + (long long )i) + (long long )x >=
0LL) && (-1LL + (long long )y) + (long long )z >= 0LL) && (7LL + (long long
)x) + (long long )z >= 0LL) && (0LL - (long long )i) + (long long )y >= 0LL)
&& (8LL - (long long )i) + (long long )x >= 0LL) && (17LL - (long long )i)
+ (long long )z >= 0LL) && i == 9) && z != -9)) || ((((((((((((-7 <= z &&
8 <= y) && z <= 2147483639) && (-16LL + (long long )i) + (long long )y >=
0LL) && (-9LL + (long long )x) + (long long )y >= 0LL) && (-9LL + (long long
)i) + (long long )x >= 0LL) && (-1LL + (long long )y) + (long long )z >= 0LL)
&& (6LL + (long long )x) + (long long )z >= 0LL) && (0LL - (long long )i)
+ (long long )y >= 0LL) && (7LL - (long long )i) + (long long )x >= 0LL) &&
(15LL - (long long )i) + (long long )z >= 0LL) && i == 8) && z != -8)) ||
((((((((((((-6 <= z && 7 <= y) && z <= 2147483640) && (-14LL + (long long
)i) + (long long )y >= 0LL) && (-8LL + (long long )x) + (long long )y >= 0LL)
&& (-8LL + (long long )i) + (long long )x >= 0LL) && (-1LL + (long long )y)
+ (long long )z >= 0LL) && (5LL + (long long )x) + (long long )z >= 0LL) &&
(0LL - (long long )i) + (long long )y >= 0LL) && (6LL - (long long )i) + (long
long )x >= 0LL) && (13LL - (long long )i) + (long long )z >= 0LL) && i ==
7) && z != -7)) || ((((((((((((-5 <= z && 6 <= y) && z <= 2147483641) && (-12LL
+ (long long )i) + (long long )y >= 0LL) && (-7LL + (long long )x) + (long
long )y >= 0LL) && (-7LL + (long long )i) + (long long )x >= 0LL) && (-1LL
+ (long long )y) + (long long )z >= 0LL) && (4LL + (long long )x) + (long
long )z >= 0LL) && (0LL - (long long )i) + (long long )y >= 0LL) && (5LL -
(long long )i) + (long long )x >= 0LL) && (11LL - (long long )i) + (long long
)z >= 0LL) && i == 6) && z != -6)) || ((((((((((((-4 <= z && 5 <= y) && z
<= 2147483642) && (-10LL + (long long )i) + (long long )y >= 0LL) && (-6LL
+ (long long )x) + (long long )y >= 0LL) && (-6LL + (long long )i) + (long
long )x >= 0LL) && (-1LL + (long long )y) + (long long )z >= 0LL) && (3LL
+ (long long )x) + (long long )z >= 0LL) && (0LL - (long long )i) + (long
long )y >= 0LL) && (4LL - (long long )i) + (long long )x >= 0LL) && (9LL -
(long long )i) + (long long )z >= 0LL) && i == 5) && z != -5)) || ((((((((((((-3
<= z && 4 <= y) && z <= 2147483643) && (-8LL + (long long )i) + (long long
)y >= 0LL) && (-5LL + (long long )x) + (long long )y >= 0LL) && (-5LL + (long
long )i) + (long long )x >= 0LL) && (-1LL + (long long )y) + (long long )z
>= 0LL) && (2LL + (long long )x) + (long long )z >= 0LL) && (0LL - (long long
)i) + (long long )y >= 0LL) && (3LL - (long long )i) + (long long )x >= 0LL)
&& (7LL - (long long )i) + (long long )z >= 0LL) && i == 4) && z != -4)) ||
((((((((((((-2 <= z && 3 <= y) && z <= 2147483644) && (-6LL + (long long )i)
+ (long long )y >= 0LL) && (-4LL + (long long )x) + (long long )y >= 0LL)
&& (-4LL + (long long )i) + (long long )x >= 0LL) && (-1LL + (long long )y)
+ (long long )z >= 0LL) && (1LL + (long long )x) + (long long )z >= 0LL) &&
(0LL - (long long )i) + (long long )y >= 0LL) && (2LL - (long long )i) + (long
long )x >= 0LL) && (5LL - (long long )i) + (long long )z >= 0LL) && i == 3)
&& z != -3)) || ((((((((((((-1 <= z && 2 <= y) && z <= 2147483645) && (-4LL
+ (long long )i) + (long long )y >= 0LL) && (-3LL + (long long )x) + (long
long )y >= 0LL) && (-3LL + (long long )i) + (long long )x >= 0LL) && (-1LL
+ (long long )y) + (long long )z >= 0LL) && (0LL - (long long )i) + (long
long )y >= 0LL) && (1LL - (long long )i) + (long long )x >= 0LL) && (3LL -
(long long )i) + (long long )z >= 0LL) && (long long )x + (long long )z >=
0LL) && i == 2) && z != -2)
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1.c
file_hash: 9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135
line: 21
column: 12
function: main
value: 1 <= x
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1.c
file_hash: 9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135
line: 21
column: 12
function: main
value: 1 <= y
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1.c
file_hash: 9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135
line: 21
column: 12
function: main
value: x != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1.c
file_hash: 9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135
line: 21
column: 12
function: main
value: y != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1.c
file_hash: 9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135
line: 21
column: 12
function: main
value: (((0 <= i && (-1LL + (long long )i) + (long long )y >= 0LL) && i != -1)
&& ((i != -2 && ((i != -3 && ((i != -4 && ((i != -5 && ((i != -6 && ((i !=
-7 && ((i != -8 && ((i != -9 && ((i != -10 && ((i != -11 && (((((((((12 <=
z && i <= 2147483635) && (-24LL + (long long )x) + (long long )z >= 0LL) &&
(-13LL + (long long )x) + (long long )y >= 0LL) && (-13LL + (long long )y)
+ (long long )z >= 0LL) && (-12LL + (long long )i) + (long long )x >= 0LL)
&& (-12LL + (long long )i) + (long long )z >= 0LL) && (-12LL - (long long
)i) + (long long )x >= 0LL) && i != -12) || (((((((((((i <= 2147483636 &&
(-22LL + (long long )x) + (long long )z >= 0LL) && (-12LL + (long long )x)
+ (long long )y >= 0LL) && (-12LL + (long long )y) + (long long )z >= 0LL)
&& (-11LL + (long long )i) + (long long )x >= 0LL) && (-11LL + (long long
)i) + (long long )z >= 0LL) && (-11LL - (long long )i) + (long long )x >=
0LL) && (10LL + (long long )y) - (long long )z >= 0LL) && (11LL + (long long
)i) - (long long )x >= 0LL) && (11LL + (long long )i) - (long long )z >= 0LL)
&& (long long )x - (long long )z >= 0LL) && z == 11))) || (((((((((((i <=
2147483637 && (-20LL + (long long )x) + (long long )z >= 0LL) && (-11LL +
(long long )x) + (long long )y >= 0LL) && (-11LL + (long long )y) + (long
long )z >= 0LL) && (-10LL + (long long )i) + (long long )x >= 0LL) && (-10LL
+ (long long )i) + (long long )z >= 0LL) && (-10LL - (long long )i) + (long
long )x >= 0LL) && (9LL + (long long )y) - (long long )z >= 0LL) && (10LL
+ (long long )i) - (long long )x >= 0LL) && (10LL + (long long )i) - (long
long )z >= 0LL) && (long long )x - (long long )z >= 0LL) && z == 10))) ||
(((((((((((i <= 2147483638 && (-18LL + (long long )x) + (long long )z >= 0LL)
&& (-10LL + (long long )x) + (long long )y >= 0LL) && (-10LL + (long long
)y) + (long long )z >= 0LL) && (-9LL + (long long )i) + (long long )x >= 0LL)
&& (-9LL + (long long )i) + (long long )z >= 0LL) && (-9LL - (long long )i)
+ (long long )x >= 0LL) && (8LL + (long long )y) - (long long )z >= 0LL) &&
(9LL + (long long )i) - (long long )x >= 0LL) && (9LL + (long long )i) - (long
long )z >= 0LL) && (long long )x - (long long )z >= 0LL) && z == 9))) || (((((((((((i
<= 2147483639 && (-16LL + (long long )x) + (long long )z >= 0LL) && (-9LL
+ (long long )x) + (long long )y >= 0LL) && (-9LL + (long long )y) + (long
long )z >= 0LL) && (-8LL + (long long )i) + (long long )x >= 0LL) && (-8LL
+ (long long )i) + (long long )z >= 0LL) && (-8LL - (long long )i) + (long
long )x >= 0LL) && (7LL + (long long )y) - (long long )z >= 0LL) && (8LL +
(long long )i) - (long long )x >= 0LL) && (8LL + (long long )i) - (long long
)z >= 0LL) && (long long )x - (long long )z >= 0LL) && z == 8))) || (((((((((((i
<= 2147483640 && (-14LL + (long long )x) + (long long )z >= 0LL) && (-8LL
+ (long long )x) + (long long )y >= 0LL) && (-8LL + (long long )y) + (long
long )z >= 0LL) && (-7LL + (long long )i) + (long long )x >= 0LL) && (-7LL
+ (long long )i) + (long long )z >= 0LL) && (-7LL - (long long )i) + (long
long )x >= 0LL) && (6LL + (long long )y) - (long long )z >= 0LL) && (7LL +
(long long )i) - (long long )x >= 0LL) && (7LL + (long long )i) - (long long
)z >= 0LL) && (long long )x - (long long )z >= 0LL) && z == 7))) || (((((((((((i
<= 2147483641 && (-12LL + (long long )x) + (long long )z >= 0LL) && (-7LL
+ (long long )x) + (long long )y >= 0LL) && (-7LL + (long long )y) + (long
long )z >= 0LL) && (-6LL + (long long )i) + (long long )x >= 0LL) && (-6LL
+ (long long )i) + (long long )z >= 0LL) && (-6LL - (long long )i) + (long
long )x >= 0LL) && (5LL + (long long )y) - (long long )z >= 0LL) && (6LL +
(long long )i) - (long long )x >= 0LL) && (6LL + (long long )i) - (long long
)z >= 0LL) && (long long )x - (long long )z >= 0LL) && z == 6))) || (((((((((((i
<= 2147483642 && (-10LL + (long long )x) + (long long )z >= 0LL) && (-6LL
+ (long long )x) + (long long )y >= 0LL) && (-6LL + (long long )y) + (long
long )z >= 0LL) && (-5LL + (long long )i) + (long long )x >= 0LL) && (-5LL
+ (long long )i) + (long long )z >= 0LL) && (-5LL - (long long )i) + (long
long )x >= 0LL) && (4LL + (long long )y) - (long long )z >= 0LL) && (5LL +
(long long )i) - (long long )x >= 0LL) && (5LL + (long long )i) - (long long
)z >= 0LL) && (long long )x - (long long )z >= 0LL) && z == 5))) || (((((((((((i
<= 2147483643 && (-8LL + (long long )x) + (long long )z >= 0LL) && (-5LL +
(long long )x) + (long long )y >= 0LL) && (-5LL + (long long )y) + (long long
)z >= 0LL) && (-4LL + (long long )i) + (long long )x >= 0LL) && (-4LL + (long
long )i) + (long long )z >= 0LL) && (-4LL - (long long )i) + (long long )x
>= 0LL) && (3LL + (long long )y) - (long long )z >= 0LL) && (4LL + (long long
)i) - (long long )x >= 0LL) && (4LL + (long long )i) - (long long )z >= 0LL)
&& (long long )x - (long long )z >= 0LL) && z == 4))) || (((((((((((i <= 2147483644
&& (-6LL + (long long )x) + (long long )z >= 0LL) && (-4LL + (long long )x)
+ (long long )y >= 0LL) && (-4LL + (long long )y) + (long long )z >= 0LL)
&& (-3LL + (long long )i) + (long long )x >= 0LL) && (-3LL + (long long )i)
+ (long long )z >= 0LL) && (-3LL - (long long )i) + (long long )x >= 0LL)
&& (2LL + (long long )y) - (long long )z >= 0LL) && (3LL + (long long )i)
- (long long )x >= 0LL) && (3LL + (long long )i) - (long long )z >= 0LL) &&
(long long )x - (long long )z >= 0LL) && z == 3))) || (((((((((((i <= 2147483645
&& (-4LL + (long long )x) + (long long )z >= 0LL) && (-3LL + (long long )x)
+ (long long )y >= 0LL) && (-3LL + (long long )y) + (long long )z >= 0LL)
&& (-2LL + (long long )i) + (long long )x >= 0LL) && (-2LL + (long long )i)
+ (long long )z >= 0LL) && (-2LL - (long long )i) + (long long )x >= 0LL)
&& (1LL + (long long )y) - (long long )z >= 0LL) && (2LL + (long long )i)
- (long long )x >= 0LL) && (2LL + (long long )i) - (long long )z >= 0LL) &&
(long long )x - (long long )z >= 0LL) && z == 2))) || (((((((((((i <= 2147483646
&& (-2LL + (long long )x) + (long long )y >= 0LL) && (-2LL + (long long )x)
+ (long long )z >= 0LL) && (-2LL + (long long )y) + (long long )z >= 0LL)
&& (-1LL + (long long )i) + (long long )x >= 0LL) && (-1LL + (long long )i)
+ (long long )z >= 0LL) && (-1LL - (long long )i) + (long long )x >= 0LL)
&& (1LL + (long long )i) - (long long )x >= 0LL) && (1LL + (long long )i)
- (long long )z >= 0LL) && (long long )x - (long long )z >= 0LL) && (long
long )y - (long long )z >= 0LL) && z == 1))) || ((((((((((((((-2LL + (long
long )x) + (long long )y >= 0LL && (-2LL + (long long )i) + (long long )x
>= 0LL) && (-2LL + (long long )i) + (long long )y >= 0LL) && (-1LL + (long
long )x) + (long long )z >= 0LL) && (-1LL + (long long )y) + (long long )z
>= 0LL) && (-1LL + (long long )i) + (long long )z >= 0LL) && (0LL - (long
long )i) + (long long )x >= 0LL) && (-1LL + (long long )x) - (long long )z
>= 0LL) && (-1LL + (long long )y) - (long long )z >= 0LL) && (-1LL + (long
long )i) - (long long )z >= 0LL) && (long long )i - (long long )x >= 0LL)
&& 0 == z) && x == i) && z == 0)
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
1887 |
2023-12-01T05:39:29+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135, sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c).
Found 10 witnesses for program sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c, 9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
114257c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2022-12-09T13:26:11Z |
|
af31c9d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-22 |
4 |
2022-12-10T22:02:22+01:00 |
|
6249c15 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2022-12-12T11:02 CET (comp) |
|
b19fadc |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
2068 |
2023-01-29T11:46:54+01:00 |
6249c15 |
b0a797c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
1965 |
2023-01-28T23:06:58+01:00 |
af31c9d |
5b7123f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
6 |
2023-01-28T17:47:09+01:00 |
114257c |
68e4e77 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2 |
2281 |
2022-12-10T21:47:32+01:00 |
|
47f608d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-1715bd67dc+ |
2281 |
2022-12-11T21:25:04+01:00 |
|
538a9a7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
2336 |
2022-12-09T23:59:52+01:00 |
|
d0cf9ff |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
10 |
2022-12-07T21:42:56+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135, sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c).
Found 8 witnesses for program sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c, 9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
e91a337 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.2.8 |
3 |
2021-12-13T21:10:31Z |
|
7b674d2 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-22 |
4 |
2021-12-06T13:41:21+01:00 |
|
0714f03 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
5 |
2021-12-09T15:27:07+01:00 |
0c8118a |
907bfc2 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
2016 |
2021-12-06T15:01:54+01:00 |
7b674d2 |
dd09509 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
2227 |
2021-12-05T17:25:56+01:00 |
|
f226f03 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-fe6f522dd3+ |
2227 |
2021-12-08T20:11:07+01:00 |
|
0c8118a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-eda176372c+ |
6 |
2021-12-09T11:01:36+01:00 |
|
e5c9248 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
10 |
2021-12-05T23:08:03+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135, sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c).
Found 4 witnesses for program sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c, 9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
05f3f0f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.2.1 |
3 |
2020-12-06T23:47:47 |
|
3d66de6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
unknown_witness |
Goblint (svcomp21-0-g82e03b87) |
3 |
2020-12-07T10:08:27 |
|
d8a25ca |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0 |
2227 |
2020-12-05T15:30:05+01:00 |
|
490a2b0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-eda176372c+ |
2281 |
2020-12-08T00:45:39+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135, sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c).
Found 2 witnesses for program sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c, 9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
29f7f53 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 1.9 |
141 |
2019-11-29T18:35:24+01:00 |
|
4fa53a0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ |
1852 |
2019-12-01T11:34:34+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135, sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c).
Found 3 witnesses for program sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c, 9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
1a8b06e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
SMACK 1.9.3 |
3 |
2018-12-08T04:23:10 |
|
30ea29b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
2133 |
2018-12-08T04:51:33+01:00 |
|
94f7543 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
2133 |
2018-12-06T04:25:44+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135, sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c).
Found 3 witnesses for program sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c, 9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
34902a6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
9 |
2017-12-03T07:44Z |
|
bd9d8ae |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 3.1 |
6 |
2017-12-01T18:51 CET (sv-comp) |
|
8b3f650 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
2LS |
11 |
2017-12-01T12:51 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135, sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c, 9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/9b244382de79ee7e63c5a39dc4ba4645eb8228d285c75cf6df9353c232d1a135.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |