Revision ed736b69
Added by Pierre-Loïc Garoche over 8 years ago
| src/backends/Horn/horn_backend.ml | ||
|---|---|---|
| 522 | 522 |
|
| 523 | 523 |
|
| 524 | 524 |
let translate fmt basename prog machines = |
| 525 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification"); |
|
| 526 | 525 |
List.iter (print_machine machines fmt) (List.rev machines); |
| 527 | 526 |
main_print machines fmt |
| 528 | 527 |
|
Also available in: Unified diff
Merge of last trunk commits
Added fbyn(expr, n, init) to encode
init -> pre (init -> pre (init -> ... pre expr))
with n occurences of init