Cover property erroneously getting refuted under bounded model checking

[ShashankVM]

Here is my project:

https://github.com/ShashankVM/hamming_encoder_decoder_bmc

The cover property here on line 65 is getting refuted. https://github.com/ShashankVM/hamming_encoder_decoder_bmc/blob/master/dut.sv#L65

Run command: ebmc -D FORMAL --bound 100 --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 --vcd wave.vcd

It is expected to be covered as there is no constraint on the input signal message that prevents it from being zero. I've not been successful in generating a waveform via VCD file that can visualize the design behaviour using the HW-CBMC tool.

k-induction and bdd also fails.

[kroening]

Can you confirm whether this is now fixed?

[ShashankVM]

Thank you, Dr. Daniel. Yes it's fixed for the bounded model checking. K-induction and BDD does not work. You may close this issue.

[kroening]

cover properties are existential. k-induction or BDDs can only refute them, not prove them.

[kroening]

Closing as fixed