Closed
Description
The command I'm running is:
ebmc ibex_id_stage.sv --top ibex_id_stage
files here: ibex.tar.gz
I'm at ebmc git commit 0ec55ad447b5109946bc46f8748da802fee2de01
The invariant violation is:
--- begin invariant violation report ---
Invariant check failed
File: flattening/boolbv_width.cpp:212 function: get_entry
Condition: false
Reason: Reached unimplemented boolbv_widtht::get_entry()
Backtrace:
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0x17bad2) [0x562f0ea7fad2]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0x17c84d) [0x562f0ea8084d]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0xb5a32) [0x562f0e9b9a32]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0x2b4fcc) [0x562f0ebb8fcc]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0x27646e) [0x562f0eb7a46e]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0x274aa0) [0x562f0eb78aa0]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0x277502) [0x562f0eb7b502]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0x28be93) [0x562f0eb8fe93]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0x2e227f) [0x562f0ebe627f]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0x2e0cc2) [0x562f0ebe4cc2]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0x2e0ff7) [0x562f0ebe4ff7]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0x2e0ff7) [0x562f0ebe4ff7]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0x37b843) [0x562f0ec7f843]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0xc8015) [0x562f0e9cc015]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0xe710d) [0x562f0e9eb10d]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0xe7369) [0x562f0e9eb369]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0xe7a88) [0x562f0e9eba88]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0x105cc6) [0x562f0ea09cc6]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0x106595) [0x562f0ea0a595]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0xd833f) [0x562f0e9dc33f]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0xa7fbf) [0x562f0e9abfbf]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0xa5f99) [0x562f0e9a9f99]
/usr/lib/x86_64-linux-gnu/libc.so.6(+0x29d90) [0x7f2aa9e29d90]
/usr/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80) [0x7f2aa9e29e40]
/home/elizabeth/hw-cbmc/src/ebmc/ebmc(+0xb09e5) [0x562f0e9b49e5]
--- end invariant violation report ---
Metadata
Metadata
Assignees
Labels
No labels