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 | |
parent | 7bd5a04fe76033d7dd6b958ea9946b70e075f28e (diff) | |
download | vericert-kvx-3144c39f4533f0936f3df0537bf470461565f5e9.tar.gz vericert-kvx-3144c39f4533f0936f3df0537bf470461565f5e9.zip |
Fix bug in scheduling
Diffstat (limited to 'src')
-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 |