Assertions on values of variables changed by child modules in next block have inconsistent values

[noloerino]

(as discussed in uclid meeting on 4/28/22)

Assertions involving variables updated by a call to the next block of a child module use a different value for the variable depending on whether it is placed before or after next.

Code

module assign_child {
    output o : boolean;

    init {
        o = false;
    }

    next {
        o' = true;
    }
}

module main {
    var o0 : boolean;
    var step : integer;
    instance child0 : assign_child(o : (o0));

    init {
        step = 0;
    }

    next {
        assert (step != 0 || !o0); // Correctly passes
        next (child0);
        assert (step != 0 || !o0); // Incorrectly fails
        step' = step + 1;
    }
    
    control {
        v = bmc_noLTL(3);
        check;
        v.print_cex(step, o0);
        print_module;
    }    
}

Output

Successfully instantiated 2 module(s).
CEX for v [Step #1] assertion @ reduced.ucl, line 25
=================================
Step #0
  step : 0
  o0 : false
=================================
=================================
Step #1
  step : 0
  o0 : true
=================================

module main {
  var step : integer; // reduced.ucl, line 15
  next // reduced.ucl, line 22
    { //
      var __ucld_2_step_lhs : integer; // line 15
      var __ucld_1_o_lhs : boolean; // line 2
      assert ((step != 0) || !(o0)); // reduced.ucl, line 23
      __ucld_1_o_lhs = true; // reduced.ucl, line 9
      o0 = __ucld_1_o_lhs; // line 0
      assert ((step != 0) || !(o0)); // reduced.ucl, line 25
      __ucld_2_step_lhs = (step + 1); // reduced.ucl, line 26
      step = __ucld_2_step_lhs; // line 0
    }
  var o0 : boolean; // reduced.ucl, line 14
  init // reduced.ucl, line 18
    { //
      var __ucld_1_o_lhs : boolean; // line 2
      var __ucld_2_step_lhs : integer; // line 15
      __ucld_1_o_lhs = o0; // line 0
      o0 = false; // reduced.ucl, line 5
      __ucld_2_step_lhs = step; // line 0
      step = 0; // reduced.ucl, line 19
    }
  control {
    v = bmc_noLTL((3,3)); // reduced.ucl, line 30
    check; // reduced.ucl, line 31
    v->print_cex((step,step), (o0,o0)); // reduced.ucl, line 32
    print_module; // reduced.ucl, line 33
  }
  // instance_var_map { 
  //   child0.o ::==> o0
  // } end_instance_var_map
  // macro_annotation_map { 
  // } end_macro_annotation_map
}

5 assertions passed.
1 assertions failed.
0 assertions indeterminate.
  PASSED -> v [Step #1] assertion @ reduced.ucl, line 23
  PASSED -> v [Step #2] assertion @ reduced.ucl, line 23
  PASSED -> v [Step #2] assertion @ reduced.ucl, line 25
  PASSED -> v [Step #3] assertion @ reduced.ucl, line 23
  PASSED -> v [Step #3] assertion @ reduced.ucl, line 25
  FAILED -> v [Step #1] assertion @ reduced.ucl, line 25
Finished execution for module: main.

Both assertions in the main module's next block read the value of o0, but the one after next(child0) incorrectly uses the next value of o0. As discussed in the uclid meeting, this may be a consequence of the child module's variable updates being inlined before assertions in the parent module are checked.