Project

General

Profile

Revision 50f7d587 src/backends/Horn/horn_backend.ml

View differences:

src/backends/Horn/horn_backend.ml
345 345

  
346 346
       Format.pp_print_newline fmt ();
347 347

  
348
       (* Rule for init *)
349
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
350
	 (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
351
	 pp_machine_init_name m.mname.node_id
352
	 (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
353

  
354 348
      (* Adding assertions *)
355 349
       (match m.mstep.step_asserts with
356 350
       | [] ->

Also available in: Unified diff