Bug #7277
opentimeout in ssh categories; several examples stop in early stages
0%
Description
File is: /home/asadis/hi-bench/challenge-bench/sv-comp17/c/ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c
File is: /home/asadis/hi-bench/challenge-bench/sv-comp17/ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c
File is: /home/asadis/hi-bench/challenge-bench/sv-comp17/ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c
Verification not successful, here is the last few lines: ...Converting
Type-checking s3_srvr.blast.08_false-unreach-call.i.cil
Generating GOTO Program
Ignoring CPROVER library
Removal of function pointers and virtual functions
Generic Property Instrumentation
LOAD Time: 2.419 sec.
Total number of claims in program...(1)
A specific claim is not set, nor any other claim specification is set.
Warrning: --claim is set to 1.
; Warning: disabling SATElite preprocessing to track proof
Use QF_UF logic.
---------checking claim # 1 ---------; Warning: disabling SATElite preprocessing to track proof
Command terminated by signal 24
timeout 200 (s)
Updated by Sepideh Asadi over 6 years ago
and also ssh-simplified categories suffer from the same problem:
File is: /home/asadis/hi-bench/challenge-bench/sv-comp17/c/ssh-simplified/s3_srvr_8_true-unreach-call.cil.c
File is: /home/asadis/hi-bench/challenge-bench/sv-comp17/c/ssh-simplified/s3_clnt_3_true-unreach-call.cil.c
File is: /home/asadis/hi-bench/challenge-bench/sv-comp17/ct/ssh-simplified/s3_srvr_4_true-unreach-call.cil.c
.
.
.
Updated by Sepideh Asadi over 6 years ago
for instance CBMC for this example take 29 second to verify this: ssh-simplified/s3_srvr_7_true-unreach-call.cil.c