summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2024-05-28 18:04:38 +0200
committerSon Ho2024-05-28 18:04:38 +0200
commit2b5186fef6932995626790af241eaed4e7cc02ae (patch)
tree72c9599c7f17423cb2f3cbc52609ad01b84a164d
parentef7792c106a1f33397c206fcb5124b5ddfe64378 (diff)
Fix a bug in SymbolicToPure.translate_loop
Diffstat (limited to '')
-rw-r--r--compiler/SymbolicToPure.ml5
1 files changed, 1 insertions, 4 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index d6d2e018..cc203040 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3529,10 +3529,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
if effect_info.stateful then mk_simpl_tuple_ty [ mk_state_ty; output ]
else output
in
- let output =
- if effect_info.can_fail && inputs <> [] then mk_result_ty output
- else output
- in
+ let output = if effect_info.can_fail then mk_result_ty output else output in
(back_info, output)
in