diff options
author | Son Ho | 2021-11-24 00:01:50 +0100 |
---|---|---|
committer | Son Ho | 2021-11-24 00:01:50 +0100 |
commit | ed8bbfc8a0cdc8474c41e16438fd80e6c491e6e2 (patch) | |
tree | 74aa671bda247b9f611c3b03b6b23d07d9039a88 | |
parent | 15613ea2e2e8f9d5b9f09c850546ef88e5ae9acd (diff) |
Insert some sanity checks
-rw-r--r-- | src/Interpreter.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 3da9853f..ca7d7a09 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -620,6 +620,9 @@ let rec activate_inactivated_mut_borrow (config : config) (io : inner_outer) (* Recursive call *) activate_inactivated_mut_borrow config io l env' | None -> + (* Some sanity checks *) + assert (not (loans_in_value sv)); + assert (not (bottom_in_value sv)); (* End the borrows which borrow from the value, at the exception of the borrow * we want to promote *) let bids = BorrowId.Set.remove l bids in |