EBMC generate wrong counter-example

[Ruochen Dai]

Dear EBMC team,

I run the EBMC to detect hardware Trojans named RS232-T600 from TrustHub, however, EBMC gave me wrong counter example.

I attached all verilog source file, the command I used to run EBMC, and generated counterexample, in the google drive: https://drive.google.com/drive/folders/194kCss9qZv_hhhU1jfY5o9ioHP_4xh5H?usp=sharing

Could you kindly help me with this problem? Thanks!

Best Regard,

Ruochen