Merge pull request #219 from AeneasVerif/son/infinite

Fix the infinite loop test

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