bench/check-ce/if_decision_branch.mlw

   1
   2 module Main
   3
   4   use int.Int
   5
   6   type path_sel_type = { mutable sel_path : bool}
   7
   8   val path_selector [@model_trace:TEMP_NAME]: path_sel_type
   9
  10 end
  11
  12
  13 module Other
  14
  15   use int.Int
  16   use Main
  17
  18   let f (a : int)
  19     ensures {result = 5}
  20   =
  21     (* The counterexample should contain the node_id 5454 here but not 121 *)
  22     if (path_selector.sel_path <- (a = 1); ([@branch_id=5454] path_selector).sel_path) then
  23       5
  24     else
  25       begin path_selector.sel_path <- true;
  26       (* The counterexample should contain the node_id 121 but not 5454 *)
  27       if (path_selector.sel_path <- (a = 5); ([@branch_id=121] path_selector).sel_path) then
  28         15
  29       else
  30         22
  31       end
  32
  33 end