summaryrefslogtreecommitdiff
path: root/src/main.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/main.ml')
-rw-r--r--src/main.ml1
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