Revision 2580acfd
Added by Teme Kahsai over 9 years ago
| src/backends/Horn/horn_backend.ml | ||
|---|---|---|
| 327 | 327 |
|
| 328 | 328 |
Format.pp_print_newline fmt (); |
| 329 | 329 |
|
| 330 |
(* Rule for init *) |
|
| 331 |
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." |
|
| 332 |
(pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs |
|
| 333 |
pp_machine_init_name m.mname.node_id |
|
| 334 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m); |
|
| 335 |
|
|
| 336 | 330 |
(* Adding assertions *) |
| 337 | 331 |
(match m.mstep.step_asserts with |
| 338 | 332 |
| [] -> |
Also available in: Unified diff
fixed a printing bug in horn backend
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@481 041b043f-8d7c-46b2-b46e-ef0dd855326e