Revision b4d9710b src/machine_code.ml
src/machine_code.ml | ||
---|---|---|
377 | 377 |
(if Stateless.check_node node_f then si else MReset o :: si), |
378 | 378 |
Utils.IMap.add o call_f j, |
379 | 379 |
d, |
380 |
reset_instance node args o r eq.eq_rhs.expr_clock @ |
|
380 |
(if Stateless.check_node node_f |
|
381 |
then [] |
|
382 |
else reset_instance node args o r call_ck) @ |
|
381 | 383 |
(control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s) |
382 | 384 |
|
383 | 385 |
(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e) |
Also available in: Unified diff