Counters incorrectly using blocking assignments in regressions and EBMC tutorial

[ShashankVM]

1. https://www.cprover.org/ebmc/manual/tutorial/
2. https://github.com/diffblue/hw-cbmc/blob/7fe06e486ef3a0d8b041e8416febf8f85e1c9a7b/regression/hw-cbmc/Counter2/main.v

Sequential logic has to use non-blocking assignment:
<=

References:

1. Avoid Assignment Mixing in Always Blocks
   Intel® Quartus® Prime Pro Edition synthesis does not allow mixed use of blocking and non-blocking assignments within ALWAYS blocks

2. Do not mix blocking and non-blocking assignments.
   Although Vivado synthesis synthesizes the design without error, mixing blocking and non-blocking assignments can cause errors during simulation.

[ShashankVM]

Please let me know if I can start working on the code fix for it.