From 0fc5b279d176b9a28709855f2671b8338ae562fc Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 12 Nov 2020 18:46:43 -0500 Subject: [PATCH] fix(LRA): invalid normalization --- src/arith/lra/fourier_motzkin.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/arith/lra/fourier_motzkin.ml b/src/arith/lra/fourier_motzkin.ml index ab695cb5..e8752c5a 100644 --- a/src/arith/lra/fourier_motzkin.ml +++ b/src/arith/lra/fourier_motzkin.ml @@ -218,8 +218,8 @@ module Make(A : ARG) (* nornalize and return maximum variable *) let normalize (self:t) : t = match self.pred with - | Geq -> mk_ ~tag:self.tag Lt (LE.neg self.le) - | Gt -> mk_ ~tag:self.tag Leq (LE.neg self.le) + | Geq -> mk_ ~tag:self.tag Leq (LE.neg self.le) + | Gt -> mk_ ~tag:self.tag Lt (LE.neg self.le) | _ -> self let find_max (self:t) : T.t option * bool =