diff options
| author | Son Ho | 2024-06-05 16:47:52 +0200 |
|---|---|---|
| committer | Son Ho | 2024-06-05 16:47:52 +0200 |
| commit | 0a0ab7c0e159e736a3187b8121d106ee76651f57 (patch) | |
| tree | 2bb2aff4f4d53d6da1408a9ea315bb5ecb8e990a /compiler | |
| parent | a6c9ab139977982f610f3d46e2e2f4c141880c3c (diff) | |
Relax more checks for borrow-checking
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/InterpreterLoopsFixedPoint.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |