Variables sometimes fail to update in counterexamples about uclid HOT 3 OPEN

module fsm {
    type op_t = enum { SET_T, SET_F };

    input imem : [bv3]op_t;
    var pc : bv3;
    var reg : boolean;
    
    init {
        pc = 0bv3;
    }

    next {
        case
            (imem[pc] == SET_T) : { reg' = true; }
            (imem[pc] == SET_F) : { reg' = false; }
        esac
        pc' = pc + 1bv3;
    }
}

module main {
    type * = fsm.*;

    var imem : [bv3]op_t;
    var step : integer;
    
    instance fsm_0 : fsm (imem : (imem));

    init {
        assume (imem[0bv3] == SET_T);
        assume (imem[1bv3] == SET_F);
        step = 0;
    }

    next {
        next (fsm_0);
        step' = step + 1;
        case
            (step == 1): {
                assert (fsm_0.reg == true);
            }
        esac
    }
        
    invariant done : (step == 1) ==> fsm_0.reg == true;

    control {
        vobj = bmc_noLTL(4);
        check;
        print_results;
        vobj.print_cex(step, imem, fsm_0.pc, fsm_0.reg);
    }
}

Successfully instantiated 2 module(s).
8 assertions passed.
1 assertions failed.
0 assertions indeterminate.
  PASSED -> vobj [Step #0] property done @ no_update_unsound.ucl, line 45
  PASSED -> vobj [Step #1] assertion @ no_update_unsound.ucl, line 40
  PASSED -> vobj [Step #1] property done @ no_update_unsound.ucl, line 45
  PASSED -> vobj [Step #2] property done @ no_update_unsound.ucl, line 45
  PASSED -> vobj [Step #3] assertion @ no_update_unsound.ucl, line 40
  PASSED -> vobj [Step #3] property done @ no_update_unsound.ucl, line 45
  PASSED -> vobj [Step #4] assertion @ no_update_unsound.ucl, line 40
  PASSED -> vobj [Step #4] property done @ no_update_unsound.ucl, line 45
  FAILED -> vobj [Step #2] assertion @ no_update_unsound.ucl, line 40
CEX for vobj [Step #2] assertion @ no_update_unsound.ucl, line 40
=================================
Step #0
  step : 0
  imem : 
	1 : SET_F
	- : SET_T
  fsm_0.pc : 0
  fsm_0.reg : false
=================================
=================================
Step #1
  step : 1
  imem : 
	1 : SET_F
	- : SET_T
  fsm_0.pc : 1
  fsm_0.reg : true
=================================
=================================
Step #2
  step : 1
  imem : 
	1 : SET_F
	- : SET_T
  fsm_0.pc : 2
  fsm_0.reg : false
=================================
Finished execution for module: main.