simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-11 13:38:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(LRA): invalid normalization

Browse source
This commit is contained in:
Simon Cruanes 2020-11-12 18:46:43 -05:00
parent 3e703cf89e
commit 0fc5b279d1
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/arith/lra/fourier_motzkin.ml
View file

@ -218,8 +218,8 @@ module Make(A : ARG)
(* nornalize and return maximum variable *) (* nornalize and return maximum variable *)
let normalize (self:t) : t = let normalize (self:t) : t =
match self.pred with match self.pred with
| Geq -> mk_ ~tag:self.tag Lt (LE.neg self.le) | Geq -> mk_ ~tag:self.tag Leq (LE.neg self.le)
| Gt -> mk_ ~tag:self.tag Leq (LE.neg self.le) | Gt -> mk_ ~tag:self.tag Lt (LE.neg self.le)
| _ -> self | _ -> self
let find_max (self:t) : T.t option * bool = let find_max (self:t) : T.t option * bool =