BDD fails with "Reached unimplemented boolbv_widtht::get_entry(natural)"

[ShashankVM]

Project link: https://github.com/ShashankVM/hamming_encoder_decoder_bmc

Run command:
ebmc -D FORMAL --bdd --top dut dut.sv cc_encoder.sv piso.sv lfsr_encoder.sv cc_decoder_ht.sv lfsr_decoder.sv buffer_reg.sv error_correction_and_detection.sv channel.sv --reset reset==1

Output:

Parsing dut.sv
Parsing cc_encoder.sv
Parsing piso.sv
Parsing lfsr_encoder.sv
Parsing cc_decoder_ht.sv
Parsing lfsr_decoder.sv
Parsing buffer_reg.sv
Parsing error_correction_and_detection.sv
Parsing channel.sv
Converting
Type-checking Verilog::buffer_reg
Type-checking Verilog::error_correction_and_detection
file error_correction_and_detection.sv line 7: Making error_correction_and_detection.error_pos a wire
Making error_correction_and_detection.error_det a wire
Making error_correction_and_detection.code_out a wire
Type-checking Verilog::lfsr_decoder
Type-checking Verilog::cc_decoder_ht
file cc_decoder_ht.sv line 17: Making cc_decoder_ht.next a wire
file cc_decoder_ht.sv line 11: Making cc_decoder_ht.clear_2 a wire
file cc_decoder_ht.sv line 11: Making cc_decoder_ht.clear_1 a wire
file cc_decoder_ht.sv line 11: Making cc_decoder_ht.valid_code_in a wire
file cc_decoder_ht.sv line 10: Making cc_decoder_ht.code_in_2 a wire
file cc_decoder_ht.sv line 10: Making cc_decoder_ht.code_in_1 a wire
Making cc_decoder_ht.code_out a wire
Making cc_decoder_ht.error_det a wire
Making cc_decoder_ht.valid_out a wire
file cc_decoder_ht.sv line 11: Making cc_decoder_ht.error_det_signal a wire
file cc_decoder_ht.sv line 13: Making cc_decoder_ht.buffer_out a wire
file cc_decoder_ht.sv line 15: Making cc_decoder_ht.syndrome_val a wire
file cc_decoder_ht.sv line 15: Making cc_decoder_ht.syndrome_val_1 a wire
file cc_decoder_ht.sv line 15: Making cc_decoder_ht.syndrome_val_2 a wire
Type-checking Verilog::lfsr_encoder
Type-checking Verilog::piso
Making piso.piso_out a wire
Type-checking Verilog::cc_encoder
Making piso(4).piso_out a wire
Making cc_encoder.valid a wire
file cc_encoder.sv line 13: Making cc_encoder.next a wire
Making cc_encoder.ready a wire
Making cc_encoder.code_out a wire
file cc_encoder.sv line 9: Making cc_encoder.lfsr_reg a wire
file cc_encoder.sv line 10: Making cc_encoder.piso_load a wire
file cc_encoder.sv line 10: Making cc_encoder.piso_out a wire
file cc_encoder.sv line 11: Making cc_encoder.piso_in a wire
Type-checking Verilog::channel
Making channel.channel_out a wire
Making channel.valid_out a wire
Type-checking Verilog::dut
Making dut.rx a wire
Making dut.tx a wire
Making dut.error_det a wire
Making dut.tx_valid a wire
Making dut.encoder_ready a wire
Making dut.rx_valid a wire
file dut.sv line 17: Making dut.channel_out a wire
file dut.sv line 15: Making dut.code_out_encoded a wire
file dut.sv line 16: Making dut.channel_valid_out a wire
file dut.sv line 29: Making dut.tx_final a wire
Building netlist
--- begin invariant violation report ---
Invariant check failed
File: flattening/boolbv_width.cpp:211 function: get_entry
Condition: false
Reason: Reached unimplemented boolbv_widtht::get_entry(natural)
Backtrace:
ebmc(+0x152aa2) [0x635ea86b6aa2]
ebmc(+0x15381d) [0x635ea86b781d]
ebmc(+0x9d072) [0x635ea8601072]
ebmc(+0x2869f9) [0x635ea87ea9f9]
ebmc(+0x32e04e) [0x635ea889204e]
ebmc(+0x32e8bf) [0x635ea88928bf]
ebmc(+0x32de9d) [0x635ea8891e9d]
ebmc(+0x32e1e8) [0x635ea88921e8]
ebmc(+0x32e074) [0x635ea8892074]
ebmc(+0x32e8bf) [0x635ea88928bf]
ebmc(+0x32de9d) [0x635ea8891e9d]
ebmc(+0x32e1e8) [0x635ea88921e8]
ebmc(+0x32e074) [0x635ea8892074]
ebmc(+0x32e8bf) [0x635ea88928bf]
ebmc(+0x32de9d) [0x635ea8891e9d]
ebmc(+0x32e1e8) [0x635ea88921e8]
ebmc(+0x32e074) [0x635ea8892074]
ebmc(+0x32e8bf) [0x635ea88928bf]
ebmc(+0x32de9d) [0x635ea8891e9d]
ebmc(+0x3304e6) [0x635ea88944e6]
ebmc(+0x331ed2) [0x635ea8895ed2]
ebmc(+0xa6909) [0x635ea860a909]
ebmc(+0xa7324) [0x635ea860b324]
ebmc(+0xdde6d) [0x635ea8641e6d]
ebmc(+0xb7943) [0x635ea861b943]
ebmc(+0x8fb7f) [0x635ea85f3b7f]
ebmc(+0x8dc59) [0x635ea85f1c59]
/lib/x86_64-linux-gnu/libc.so.6(+0x2a1ca) [0x7912b3e2a1ca]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x8b) [0x7912b3e2a28b]
ebmc(+0x98015) [0x635ea85fc015]


--- end invariant violation report ---
Aborted (core dumped)

Note: I later added an ifdef so covers are not included by default.