From 4c29c8ac811da52bf630a24b04b5f9ca67aa67c6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 8 Mar 2024 21:35:27 +0100
Subject: Fix a last issue

---
 compiler/InterpreterLoops.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'compiler/InterpreterLoops.ml')

diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 55836e48..1d774e0e 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -190,6 +190,9 @@ let eval_loop_symbolic (config : config) (meta : meta)
        Moreover, we list the borrows in the same order as the loans (this
        is important in {!SymbolicToPure}, where we expect the given back
        values to have a specific order.
+
+       Also, we filter the backward functions which and
+       return nothing.
     *)
     let compute_abs_given_back_tys (abs : abs) : rty list =
       let is_borrow (av : typed_avalue) : bool =
-- 
cgit v1.2.3