From c9f01415918511ff28197a0f3d3a1be43026145f Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 30 Oct 2019 15:00:57 -0500 Subject: [PATCH] fix(mini-cc): handle `not` properly --- src/mini-cc/Sidekick_mini_cc.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/mini-cc/Sidekick_mini_cc.ml b/src/mini-cc/Sidekick_mini_cc.ml index d260d737..a3e604f9 100644 --- a/src/mini-cc/Sidekick_mini_cc.ml +++ b/src/mini-cc/Sidekick_mini_cc.ml @@ -210,6 +210,10 @@ module Make(A: ARG) = struct (fun k->k "(@[mini-cc.congruence-by-eq@ %a@ %a@])" Node.pp n Node.pp n2); self.combine <- (n,n2) :: self.combine; ) + | Some (Not u) when Node.equal u self.true_ -> + self.combine <- (n,self.false_) :: self.combine + | Some (Not u) when Node.equal u self.false_ -> + self.combine <- (n,self.true_) :: self.combine | Some s -> Log.debugf 5 (fun k->k "(@[mini-cc.update-sig@ %a@])" Signature.pp s); match Sig_tbl.find self.sig_tbl s with