diff options
author | Son Ho | 2024-03-08 19:43:45 +0100 |
---|---|---|
committer | Son Ho | 2024-03-08 19:43:45 +0100 |
commit | 677d7678f6b88075332a7e9ee6befc7c887b6a4f (patch) | |
tree | 62d05610b80418a03b403f5db6590b0c777a954f | |
parent | cd99485fa2493697b2b3775a5cae80bf9bf58a99 (diff) |
Fix an issue with the loops
-rw-r--r-- | compiler/SymbolicToPure.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 51a5da15..06294af7 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1988,7 +1988,13 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool) (* Backward *) (* Group the variables in which we stored the values we need to give back. * See the explanations for the [SynthInput] case in [translate_end_abstraction] *) - let backward_outputs = Option.get ctx.backward_outputs in + (* It can happen that we did not end any output abstraction, because the + loop didn't use borrows corresponding to the region we just ended. + If this happens, there are no backward outputs. + *) + let backward_outputs = + match ctx.backward_outputs with Some outputs -> outputs | None -> [] + in let field_values = List.map mk_texpression_from_var backward_outputs in mk_simpl_tuple_texpression field_values in |