From 0a0ab7c0e159e736a3187b8121d106ee76651f57 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 16:47:52 +0200
Subject: Relax more checks for borrow-checking

---
 compiler/InterpreterLoopsFixedPoint.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'compiler')

diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 0d770e80..3760d15a 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -683,9 +683,10 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span)
     (* If we generate a translation, we check that all the regions need to end
        - this is not necessary per se, but if it doesn't happen it is bizarre and worth investigating...
        We need this check for now for technical reasons to make the translation work.
+       If we only borrow-check, we can ignore this.
     *)
     sanity_check __FILE__ __LINE__
-      (AbstractionId.Set.equal !aids_union !fp_aids)
+      (!Config.borrow_check || AbstractionId.Set.equal !aids_union !fp_aids)
       span;
 
     (* Merge the abstractions which need to be merged, and compute the map from
-- 
cgit v1.2.3