diff options
author | Son Ho | 2021-11-30 10:02:30 +0100 |
---|---|---|
committer | Son Ho | 2021-11-30 10:02:30 +0100 |
commit | a64dfa5f21beec47706c614f4fe1c426f9c9a0c8 (patch) | |
tree | ebef7a12c4cecfa587f52c76a4ae01a8bda36230 | |
parent | f5e1f3338acb9e6282b5c6d60aa10ef81172a129 (diff) |
Fix another bug
-rw-r--r-- | src/Interpreter.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index e24f565e..38c5851c 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -875,12 +875,16 @@ let rec activate_inactivated_mut_borrow (config : C.config) (io : inner_outer) | None -> (* No loan to end inside the value *) (* Some sanity checks *) + L.log#ldebug + (lazy + ("activate_inactivated_mut_borrow: resulting value:\n" + ^ V.show_typed_value sv)); assert (not (loans_in_value sv)); assert (not (bottom_in_value sv)); let check_not_inactivated bc = match bc with V.InactivatedMutBorrow _ -> false | _ -> true in - assert (not (check_borrows_in_value check_not_inactivated sv)); + assert (check_borrows_in_value check_not_inactivated sv); (* End the borrows which borrow from the value, at the exception of the borrow we want to promote *) let bids = V.BorrowId.Set.remove l bids in |