1b22e29 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T07:27:34Z |
|
24e5431 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
16 |
2023-12-01T03:52:16+01:00 |
34749ee |
a066781 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:41:33+01:00 |
|
1585e91 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:38 CET (comp) |
|
c72019c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
5 |
2023-12-02T11:45:45Z |
|
7612e84 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T15:18:30Z |
|
efb511d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Kojak |
5 |
2023-12-03T01:32:23Z |
|
34749ee |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
12 |
2023-12-01T01:36:31Z |
|
8f970d3 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-12-20T03:41:16+01:00 |
1585e91 |
dbd9e08 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-12-19T14:43:50+01:00 |
e6b8109 |
40e2f3d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-12-19T04:24:56+01:00 |
858ce10 |
675d1cb |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-12-17T06:04:27+01:00 |
98a6b17 |
0722432 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-12-04T11:38:41+01:00 |
c72019c |
a7cb86f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-12-04T02:00:23+01:00 |
f7b057a |
2220b27 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-12-03T18:30:24+01:00 |
a066781 |
cd0d37d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-12-03T09:58:29+01:00 |
1b22e29 |
851f454 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-12-03T06:01:27+01:00 |
efb511d |
f7f62c4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-11-30T23:55:05+01:00 |
eee786f |
b48befe |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-11-30T11:57:43+01:00 |
291b4bb |
291b4bb |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-11-30T08:41:49+01:00 |
|
7b96a62 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-11-29T18:19:01+01:00 |
7612e84 |
c49745c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-11-29T08:02:45+01:00 |
0965b1c |
f7b057a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
4 |
2023-12-03T23:05:20+01:00 |
|
98a6b17 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
4 |
2023-12-17T04:33:19+01:00 |
|
858ce10 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
4 |
2023-12-18T21:43:40+01:00 |
|
0965b1c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
5 |
2023-11-29T00:09:53Z |
|
eee786f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
2LS |
8 |
2023-11-30T09:38:11+01:00 |
|
6b520d2 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
VERIFUZZ |
3 |
2023-12-01T22:22:55Z |
|
446a0d7 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.3 |
5 |
2023-11-30T05:21:17+01:00 |
|
f26162a |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Bubaak |
3 |
2023-12-05T07:33:16Z |
|
4d40897 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Bubaak |
3 |
2023-12-04T05:27:46Z |
|
6cf9e7a |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
2LS |
7 |
2023-11-30T23:19:50+01:00 |
|
bb36b64 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: dc58e277-e6fc-4b1e-a331-403168999665
creation_time: '2023-12-02T12:45:45+01:00'
producer:
name: Taipan
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e77b86b2-5662-4057-8ff8-d17e0ae93bfd/sv-benchmarks/c/termination-restricted-15/Swingers.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e77b86b2-5662-4057-8ff8-d17e0ae93bfd/sv-benchmarks/c/termination-restricted-15/Swingers.c
: 5255c645b81d71ec22a6f16f291eb82db3a98401495220a0b410dfa7eea5b30a
specification: |+
CHECK( init(main()), LTL(G ! overflow) )
data_model: 64bit
language: C
content:
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_e77b86b2-5662-4057-8ff8-d17e0ae93bfd/sv-benchmarks/c/termination-restricted-15/Swingers.c
file_hash: 5255c645b81d71ec22a6f16f291eb82db3a98401495220a0b410dfa7eea5b30a
line: 12
column: 0
function: main
value: (30 == (samantha + bob))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-04T12:00:42+01:00 |
|
bd2333d |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: c1a62a7f-5693-4a57-8731-cac27b49a2c8
creation_time: '2023-11-29T01:09:53+01:00'
producer:
name: Automizer
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_79a6e87e-d6b6-42d3-b89c-629af3fd6ec8/sv-benchmarks/c/termination-restricted-15/Swingers.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_79a6e87e-d6b6-42d3-b89c-629af3fd6ec8/sv-benchmarks/c/termination-restricted-15/Swingers.c
: 5255c645b81d71ec22a6f16f291eb82db3a98401495220a0b410dfa7eea5b30a
specification: |+
CHECK( init(main()), LTL(G ! overflow) )
data_model: 64bit
language: C
content:
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_79a6e87e-d6b6-42d3-b89c-629af3fd6ec8/sv-benchmarks/c/termination-restricted-15/Swingers.c
file_hash: 5255c645b81d71ec22a6f16f291eb82db3a98401495220a0b410dfa7eea5b30a
line: 12
column: 0
function: main
value: (30 == (samantha + bob))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-29T07:47:09+01:00 |
|
f170d51 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 9d5d05b7-917d-41a1-b3d5-72992d01b0d2
creation_time: '2023-12-03T02:32:23+01:00'
producer:
name: Kojak
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_bd0db315-24cf-4c8f-91fe-417350984969/sv-benchmarks/c/termination-restricted-15/Swingers.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_bd0db315-24cf-4c8f-91fe-417350984969/sv-benchmarks/c/termination-restricted-15/Swingers.c
: 5255c645b81d71ec22a6f16f291eb82db3a98401495220a0b410dfa7eea5b30a
specification: |+
CHECK( init(main()), LTL(G ! overflow) )
data_model: 64bit
language: C
content:
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_bd0db315-24cf-4c8f-91fe-417350984969/sv-benchmarks/c/termination-restricted-15/Swingers.c
file_hash: 5255c645b81d71ec22a6f16f291eb82db3a98401495220a0b410dfa7eea5b30a
line: 12
column: 0
function: main
value: (((samantha + bob) <= 30) && (30 <= (samantha + bob)))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-03T05:44:53+01:00 |
|
732f91e |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: 3ff08082-8bc1-44fc-8d4a-c0997771a9b8
creation_time: 2023-12-01T01:36:31Z
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/Swingers.c'''
task:
input_files:
- ../../sv-benchmarks/c/termination-restricted-15/Swingers.c
input_file_hashes:
../../sv-benchmarks/c/termination-restricted-15/Swingers.c: 5255c645b81d71ec22a6f16f291eb82db3a98401495220a0b410dfa7eea5b30a
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/Swingers.c
file_hash: 5255c645b81d71ec22a6f16f291eb82db3a98401495220a0b410dfa7eea5b30a
line: 12
column: 11
function: main
value: (-30LL + (long long )bob) + (long long )samantha >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/Swingers.c
file_hash: 5255c645b81d71ec22a6f16f291eb82db3a98401495220a0b410dfa7eea5b30a
line: 12
column: 11
function: main
value: (30LL - (long long )bob) - (long long )samantha >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/Swingers.c
file_hash: 5255c645b81d71ec22a6f16f291eb82db3a98401495220a0b410dfa7eea5b30a
line: 12
column: 11
function: main
value: ((((((-30LL + (long long )bob) + (long long )temp >= 0LL && (0LL - (long
long )samantha) + (long long )temp >= 0LL) && (30LL - (long long )bob) - (long
long )temp >= 0LL) && (long long )samantha - (long long )temp >= 0LL) && samantha
== temp) && ((((((((((-26LL + (long long )samantha) + (long long )temp >=
0LL && (4LL - (long long )bob) + (long long )samantha >= 0LL) && (4LL - (long
long )bob) + (long long )temp >= 0LL) && ((((((((((((((((((((((((0 <= bob
&& 0 <= samantha) && 0 <= temp) && 4 <= samantha) && 4 <= temp) && 13 <= bob)
&& bob <= 100) && bob <= 127) && samantha <= 17) && samantha <= 127) && temp
<= 17) && temp <= 127) && (4LL + (long long )bob) - (long long )samantha >=
0LL) && (4LL + (long long )bob) - (long long )temp >= 0LL) && (34LL - (long
long )samantha) - (long long )temp >= 0LL) && bob % 4 == 1) && samantha %
4 == 1) && temp % 4 == 1) && bob != 0) && samantha != 0) && temp != 0) &&
(bob == 13 || bob == 17)) && (samantha == 13 || samantha == 17)) && (temp
== 13 || temp == 17)) || (((((((((-4LL + (long long )bob) - (long long )samantha
>= 0LL && (-4LL + (long long )bob) - (long long )temp >= 0LL) && (26LL - (long
long )samantha) - (long long )temp >= 0LL) && 13 == samantha) && 13 == temp)
&& 17 == bob) && bob == 17) && samantha == 13) && temp == 13))) || ((((((((((((-34LL
+ (long long )samantha) + (long long )temp >= 0LL && (-4LL - (long long )bob)
+ (long long )samantha >= 0LL) && (-4LL - (long long )bob) + (long long )temp
>= 0LL) && (4LL + (long long )bob) - (long long )samantha >= 0LL) && (4LL
+ (long long )bob) - (long long )temp >= 0LL) && (34LL - (long long )samantha)
- (long long )temp >= 0LL) && 13 == bob) && 17 == samantha) && 17 == temp)
&& bob == 13) && samantha == 17) && temp == 17)) || ((((((((((((-26LL + (long
long )samantha) + (long long )temp >= 0LL && (4LL - (long long )bob) + (long
long )samantha >= 0LL) && (4LL - (long long )bob) + (long long )temp >= 0LL)
&& (-4LL + (long long )bob) - (long long )samantha >= 0LL) && (-4LL + (long
long )bob) - (long long )temp >= 0LL) && (26LL - (long long )samantha) - (long
long )temp >= 0LL) && 13 == samantha) && 13 == temp) && 17 == bob) && bob
== 17) && samantha == 13) && temp == 13)) || ((((((((((((-34LL + (long long
)samantha) + (long long )temp >= 0LL && (-4LL - (long long )bob) + (long long
)samantha >= 0LL) && (-4LL - (long long )bob) + (long long )temp >= 0LL) &&
(4LL + (long long )bob) - (long long )samantha >= 0LL) && (4LL + (long long
)bob) - (long long )temp >= 0LL) && (34LL - (long long )samantha) - (long
long )temp >= 0LL) && 13 == bob) && 17 == samantha) && 17 == temp) && bob
== 13) && samantha == 17) && temp == 17)) || ((((((((((((-26LL + (long long
)samantha) + (long long )temp >= 0LL && (4LL - (long long )bob) + (long long
)samantha >= 0LL) && (4LL - (long long )bob) + (long long )temp >= 0LL) &&
(-4LL + (long long )bob) - (long long )samantha >= 0LL) && (-4LL + (long long
)bob) - (long long )temp >= 0LL) && (26LL - (long long )samantha) - (long
long )temp >= 0LL) && 13 == samantha) && 13 == temp) && 17 == bob) && bob
== 17) && samantha == 13) && temp == 13)) || ((((((((((((-34LL + (long long
)samantha) + (long long )temp >= 0LL && (-4LL - (long long )bob) + (long long
)samantha >= 0LL) && (-4LL - (long long )bob) + (long long )temp >= 0LL) &&
(4LL + (long long )bob) - (long long )samantha >= 0LL) && (4LL + (long long
)bob) - (long long )temp >= 0LL) && (34LL - (long long )samantha) - (long
long )temp >= 0LL) && 13 == bob) && 17 == samantha) && 17 == temp) && bob
== 13) && samantha == 17) && temp == 17)) || ((((((((((((-26LL + (long long
)samantha) + (long long )temp >= 0LL && (4LL - (long long )bob) + (long long
)samantha >= 0LL) && (4LL - (long long )bob) + (long long )temp >= 0LL) &&
(-4LL + (long long )bob) - (long long )samantha >= 0LL) && (-4LL + (long long
)bob) - (long long )temp >= 0LL) && (26LL - (long long )samantha) - (long
long )temp >= 0LL) && 13 == samantha) && 13 == temp) && 17 == bob) && bob
== 17) && samantha == 13) && temp == 13))) || ((((((((((((((2147483631LL +
(long long )samantha) + (long long )temp >= 0LL && (2147483635LL + (long long
)bob) + (long long )temp >= 0LL) && (-4LL - (long long )bob) + (long long
)samantha >= 0LL) && (2147483661LL - (long long )bob) + (long long )temp >=
0LL) && (2147483665LL - (long long )samantha) + (long long )temp >= 0LL) &&
(4LL + (long long )bob) - (long long )samantha >= 0LL) && (2147483630LL +
(long long )samantha) - (long long )temp >= 0LL) && (2147483634LL + (long
long )bob) - (long long )temp >= 0LL) && (2147483660LL - (long long )bob)
- (long long )temp >= 0LL) && (2147483664LL - (long long )samantha) - (long
long )temp >= 0LL) && 13 == bob) && 17 == samantha) && bob == 13) && samantha
== 17)
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
12 |
2023-12-01T04:33:21+01:00 |
|