Project

General

Profile

Bug #7272

unusual long symext time

Added by Sepideh Asadi about 1 year ago. Updated about 1 year ago.

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

History

#1 Updated by Karine Even Mendoza about 1 year 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.

Also available in: Atom PDF