diff options
| -rw-r--r-- | compiler/SymbolicToPure.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 120689e5..81d81789 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -2437,6 +2437,11 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = (* Update the context for the loop body *) let ctx_loop = { ctx_end with inside_loop = true } in + (* Add the input state *) + let input_state = + if ctx.sg.info.effect_info.stateful then Some ctx.state_var else None + in + (* Translate the loop body *) let loop_body = translate_expression loop.loop_expr ctx_loop in @@ -2448,7 +2453,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = loop_id; fuel0 = ctx.fuel0; fuel = ctx.fuel; - input_state = (if !Config.use_state then Some ctx.state_var else None); + input_state; inputs; inputs_lvs; back_output_tys; |