Skip to content

Bug in 2ls k-induction #85

Open
Open
@rajdeep87

Description

@rajdeep87

K-induction proof seems to be buggy in 2ls. The following benchmark reproduce the bug.
https://github.com/rajdeep87/verilog-c/tree/master/safe/hwmcc15/6s177

@peterschrammel The proof fails showing "k-induction counterexample found after 0 unwinding(s)". However, CBMC proves it safe for 100 unwindings. Also, the benchmark is SAFE for more than 100 unwindings.
Command line option used : --k-induction --inline --havoc --competition mode

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions