BMC/Temp Ind Mismatch?

Makefile

my_hello1: my_hello1.smt2
	yosys-smtbmc -s z3 --dump-smt2 my_hello1_full_bmc.smt2 --dump-vcd my_hello1_bmc.vcd my_hello1.smt2
	yosys-smtbmc -s z3 -i --dump-smt2 my_hello1_full_tmp.smt2 --dump-vcd my_hello1_tmp.vcd my_hello1.smt2

my_hello1.smt2: my_hello1.v
	yosys -ql my_hello1.yslog \
		-p 'read_verilog -formal my_hello1.v' \
		-p 'prep -top my_hello -nordff' \
		-p 'clk2fflogic; opt_clean' \
		-p 'write_verilog my_hello_clk2ff.v' \
		-p 'write_smt2 -wires my_hello1.smt2'

clean::
	rm -f my_hello1.yslog *.smt2 my_hello1*.vcd my_hello_clk2ff.v

my_hello1.v

module my_hello(input clk, input rst, output [3:0] cnt);
  reg [3:0] cnt = 0;
  
  //reg my_clk = 0;
  
  /* always @(posedge clk) begin
    my_clk <= ~my_clk;
  end */

  //always @(posedge my_clk) begin
  always @(posedge clk) begin
    if (rst)
      cnt <= 0;
    else
      cnt <= cnt + 1;
  end

`ifdef FORMAL
  //initial begin
  //  assume(rst);
  //end
  
  assume property (cnt != 3);
  assert property (cnt != 5);

endmodule