aboutsummaryrefslogtreecommitdiffstats
path: root/backend/CSE2.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/CSE2.v')
-rw-r--r--backend/CSE2.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v
index a818996b..a76104af 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -296,7 +296,7 @@ Definition kill_sym_val_mem (sv: sym_val) :=
Definition kill_mem (rel : RELATION.t) :=
mkrel
- (PTree.filter1 (fun x => negb (kill_sym_val_mem x)) (var_to_sym rel))
+ (PTree.remove_t (var_to_sym rel) (mem_used rel))
pset_empty.