Skip to content

CSmith test with random seed 1670693558 results in invariant failure #7426

@tautschnig

Description

@tautschnig

From https://github.com/diffblue/cbmc/actions/runs/3665207680/jobs/6196126610 (PR #7425, but the changes in this PR seem unrelated).

CBMC version: 5.72.1 (7326b02)
Operating system: Linux
Exact command line resulting in the issue: cbmc --unwind 257 --no-unwinding-assertions --object-bits 13 t_9.i (obtained using random seed 1670693558)
What behaviour did you expect: Report "VERIFICATION SUCCESSFUL"
What happened instead: Invariant failure:

[...]
converting SSA
--- begin invariant violation report ---
Invariant check failed
File: flattening/boolbv_typecast.cpp:430 function: type_conversion
Condition: src_width == dest_width
Reason: source bitvector width shall equal the destination bitvector width
Backtrace:
cbmc(+0x2d01f0) [0x55722e7be1f0]
cbmc(+0x2d0799) [0x55722e7be799]
cbmc(+0x1d2a78) [0x55722e6c0a78]
cbmc(+0x86103d) [0x55722ed4f03d]
cbmc(+0x86173d) [0x55722ed4f73d]
cbmc(+0x822af6) [0x55722ed10af6]
cbmc(+0x86cb96) [0x55722ed5ab96]
cbmc(+0x8261c0) [0x55722ed141c0]
cbmc(+0x82211a) [0x55722ed1011a]
cbmc(+0x8221e8) [0x55722ed101e8]
cbmc(+0x7d8671) [0x55722ecc6671]
cbmc(+0x7e0e26) [0x55722eccee26]
cbmc(+0x7e19d2) [0x55722eccf9d2]
cbmc(+0x5d98b4) [0x55722eac78b4]
cbmc(+0x5d9d35) [0x55722eac7d35]
cbmc(+0x5e8ef5) [0x55722ead6ef5]
cbmc(+0x3b3139) [0x55722e8a1139]
cbmc(+0x3afc8e) [0x55722e89dc8e]
cbmc(+0x1c4c8f) [0x55722e6b2c8f]
cbmc(+0x1b5e79) [0x55722e6a3e79]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f9f94f46083]
cbmc(+0x1c582e) [0x55722e6b382e]


--- end invariant violation report ---

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions