summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Invariants.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml
index ba069bc4..66a5e5ac 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -708,7 +708,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_regions info.ty then assert (info.env_count <= 1);
+ assert (info.env_count <= 1 || type_is_primitively_copyable info.ty)
in
M.iter check_info !infos