Actions
Bug #7272
openunusual long symext time
Status:
New
Priority:
Normal
Assignee:
-
Start date:
03/05/2018
Due date:
% Done:
0%
Estimated time:
Description
File: ssh-simplified/s3_srvr_8_true-unreach-call.cil.c
----------------------------------------
How to run:
./hifrog --sum-theoref --unwind 10 file.c
The result is UNSAT , in 28 second in CBMC,
But Hifrog spend so much time for symex! 230 second
Updated by Karine Even Mendoza over 6 years ago
A result of wrong evaluation of guards in HiFrog, still checking what is the cause of it.
"False" guards are not evaluate correctly, the original (full) equation stays there and causes the long processing time.
Actions