From 677d7678f6b88075332a7e9ee6befc7c887b6a4f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 8 Mar 2024 19:43:45 +0100
Subject: Fix an issue with the loops

---
 compiler/SymbolicToPure.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'compiler')

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
-- 
cgit v1.2.3