Bug #5846
Recursion not working properly
Status:
Closed
Priority:
High
Assignee:
-
Start date:
10/11/2017
Due date:
% Done:
100%
Estimated time:
Description
Recursion ignores the max_unwind bound and continues unrolling if the verification is no successful.
Source code in the attachment.
Run with params: --unwind 2
For prop and qflra it continues unrolling till 4th or 5th iteration where the verification succeeds, for qfuf continues unrolling indefinitely.
History
#1 Updated by Martin Blicha over 6 years ago
- Status changed from New to Closed
- % Done changed from 0 to 100
It turns out this is the desired behaviour of HiFrog for recursion. The --unwind bound is only for loops. while the bound for recursion is detected automatically in the process, see:http://verify.inf.usi.ch/sites/default/files/fedyukovich_smbf14.pdf