diff options
author | Son Ho | 2023-01-06 18:41:02 +0100 |
---|---|---|
committer | Son HO | 2023-02-03 11:21:46 +0100 |
commit | 586e756761de2730a5147bf19a9f62f455690a08 (patch) | |
tree | bd29b86a021f2a4b775c9156e16956b701018cc6 /compiler | |
parent | c1473942f0aa0dba524eb7fe08f149488ecc2a6d (diff) |
Fix a minor issue
Diffstat (limited to '')
-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; |