aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/IfConversion.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/hls/IfConversion.v')
-rw-r--r--src/hls/IfConversion.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 67bd2a8..7221c28 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -60,7 +60,7 @@ Definition if_convert_block (c: code) (p: predicate) (bb: bblock) : bblock :=
| Some bb1, Some bb2 =>
let bb1' := List.map (map_if_convert (Plit (true, p))) bb1.(bb_body) in
let bb2' := List.map (map_if_convert (Plit (false, p))) bb2.(bb_body) in
- mk_bblock (List.concat (bb.(bb_body) :: ((RBsetpred cond args p) :: bb1') :: bb2' :: nil))
+ mk_bblock (List.concat (bb.(bb_body) :: ((RBsetpred None cond args p) :: bb1') :: bb2' :: nil))
(RBpred_cf (Plit (true, p)) bb1.(bb_exit) bb2.(bb_exit))
| _, _ => bb
end