How to do correct verification correctly using hw-cbmc

[Niccolo Hamilton]

I find that current hw-cbmc will get false result when verifying all programs including the testbenches given in hw-cbmc repositories.  When verifying the example in   regression/hw-cbmc/Always-Assign, all assertion gets a result "failed".

And even worse, some verification will simply crash and throw error, like invariant violation error when verifying the example in   regression/hw-cbmc/Combinational1 .

I am not sure if that is because I make some mistake in verification, but these examples can be verified successfully with the hw-cbmc binary provided by repository of experiment of your FM16 and TACAS16 paper.
And I did make successful verification with the hw-cbmc binary you provide with the researches.

It is thrilled to see you perfecting ebmc for SystemVerilog, and I wish you may pay some attention hw-cbmc.