diff --git a/src/printers/pyrat.ml b/src/printers/pyrat.ml index d80dc5f54910b78d278facfb0e63a50c31a5ff57..51573a768f143068e1f180943935d800543a6cc1 100644 --- a/src/printers/pyrat.ml +++ b/src/printers/pyrat.ml @@ -96,20 +96,24 @@ let rec negate_term info t = (* Negate float relational symbols. *) let ls_neg = if Term.ls_equal ls info.ls_rel_float.le - || Term.ls_equal ls info.ls_rel_float.lt + then info.ls_rel_float.gt + else if Term.ls_equal ls info.ls_rel_float.lt then info.ls_rel_float.ge else if Term.ls_equal ls info.ls_rel_float.ge - || Term.ls_equal ls info.ls_rel_float.gt + then info.ls_rel_float.lt + else if Term.ls_equal ls info.ls_rel_float.gt then info.ls_rel_float.le else ls in (* Negate real relational symbols. *) let ls_neg = if Term.ls_equal ls info.ls_rel_real.le - || Term.ls_equal ls info.ls_rel_real.lt + then info.ls_rel_real.gt + else if Term.ls_equal ls info.ls_rel_real.lt then info.ls_rel_real.ge else if Term.ls_equal ls info.ls_rel_real.ge - || Term.ls_equal ls info.ls_rel_real.gt + then info.ls_rel_real.lt + else if Term.ls_equal ls info.ls_rel_real.gt then info.ls_rel_real.le else ls_neg in