diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-10-20 18:44:47 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-10-20 18:44:47 +0100 |
| commit | 3144c39f4533f0936f3df0537bf470461565f5e9 (patch) | |
| tree | b5cd0c6db629d0381a203fd8b6f6f48b4618558c /src/hls/Schedule.ml | |
| parent | 7bd5a04fe76033d7dd6b958ea9946b70e075f28e (diff) | |
| download | vericert-3144c39f4533f0936f3df0537bf470461565f5e9.tar.gz vericert-3144c39f4533f0936f3df0537bf470461565f5e9.zip | |
Fix bug in scheduling
Diffstat (limited to 'src/hls/Schedule.ml')
| -rw-r--r-- | src/hls/Schedule.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index 37e6f42..e521214 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -420,7 +420,7 @@ let transf_htl r c (schedule : (int * int) list IMap.t) = (add_schedules r bb_body' min_state (P.to_int i)) (IMap.to_seq i_sched_tree |> List.of_seq) >>= fun _ -> - translate_control_flow r (P.of_int (P.to_int i - max_state)) ctrl_flow + translate_control_flow r (P.of_int (P.to_int i - max_state - 1)) ctrl_flow | _ -> coqstring_of_camlstring "Illegal state reached in scheduler" |> Errors.msg |> error |