Add an option to eagerly end abstractions if a function has return type

unit and the abstractions don't contain loans

1 files changed, 1 insertions, 0 deletions

diff --git a/src/main.ml b/src/main.ml
index 3fb162f3..6b1083f5 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -159,6 +159,7 @@ let () =
           C.check_invariants = not !no_check_inv;
           greedy_expand_symbolics_with_borrows = true;
           allow_bottom_below_borrow = true;
+          return_unit_end_abs_with_no_loans = true;
         }
       in