From d6d65a785aa14fc6d530823d96c75a336816bcd7 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 16 Oct 2019 05:22:41 -0700 Subject: [PATCH] [sledge] Remove left-over SSA assertion Reviewed By: bennostein Differential Revision: D17856383 fbshipit-source-id: 34c347f3e --- sledge/src/symbheap/sh_domain.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/sledge/src/symbheap/sh_domain.ml b/sledge/src/symbheap/sh_domain.ml index 44eeb4410..473b8c75d 100644 --- a/sledge/src/symbheap/sh_domain.ml +++ b/sledge/src/symbheap/sh_domain.ml @@ -38,8 +38,7 @@ let exec_move q res = let exec_inst pre inst = [%Trace.info "@[<2>exec inst %a from@ @[{ %a@ }@]@]" Llair.Inst.pp inst Sh.pp pre] ; - assert (Set.disjoint (Sh.fv pre) (Reg.Set.vars (Llair.Inst.locals inst))) ; - match inst with + match (inst : Llair.inst) with | Move {reg_exps; _} -> Some (Exec.move pre