Project

General

Profile

Revision e4edf171 src/backends/Horn/horn_backend_collecting_sem.ml

View differences:

src/backends/Horn/horn_backend_collecting_sem.ml
49 49
  (* Init case *)
50 50
  let _ = 
51 51
    (* Special case when the main node is stateless *)
52
    if is_stateless machine then (
52
    if Machine_code_common.is_stateless machine then (
53 53
      let step_name = pp_machine_stateless_name in
54 54
      fprintf fmt "; Initial set: One Step(m,x)  -- Stateless node! @.";
55 55
      fprintf fmt "(declare-rel INIT_STATE ())@.";
......
86 86
  in
87 87

  
88 88
  let step_name = 
89
    if is_stateless machine then 
89
    if Machine_code_common.is_stateless machine then 
90 90
      pp_machine_stateless_name
91 91
    else
92 92
      pp_machine_step_name
......
142 142

  
143 143
    (* Special case when the cex node is stateless *)
144 144
  let reset_name, step_name =
145
    if is_stateless machine then
145
    if Machine_code_common.is_stateless machine then
146 146
      pp_machine_stateless_name, pp_machine_stateless_name
147 147
    else
148 148
      pp_machine_reset_name, pp_machine_step_name

Also available in: Unified diff