summaryrefslogtreecommitdiff
path: root/src/Invariants.ml
diff options
context:
space:
mode:
authorSon Ho2022-01-18 23:03:55 +0100
committerSon Ho2022-01-18 23:03:55 +0100
commitc0f230dc6c331e9eb120900e8c31a03e1f5ab476 (patch)
tree16ff97c6af5e85baab2e7f1af5456bd2854e057b /src/Invariants.ml
parentcdef093fedaadcc5694cb9f7d63a4bf9814d5573 (diff)
Remove ty_has_regions and use ty_has_borrows instead
Diffstat (limited to 'src/Invariants.ml')
-rw-r--r--src/Invariants.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 5b77e13c..67084684 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -707,7 +707,8 @@ let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit =
(* Check *)
let check_info _id info =
assert (info.env_count = 0 || info.aproj_borrows = []);
- if ty_has_regions info.ty then assert (info.env_count <= 1);
+ if ty_has_borrows ctx.type_context.type_infos info.ty then
+ assert (info.env_count <= 1);
assert (info.env_count <= 1 || ty_is_primitively_copyable info.ty)
in
M.iter check_info !infos