diff --git a/src/printers/marabou.ml b/src/printers/marabou.ml index 817c0940d2c3924bbf3782d2461123acea04632d..823782a481186b8ed05bad147c565068ef0cc091 100644 --- a/src/printers/marabou.ml +++ b/src/printers/marabou.ml @@ -76,10 +76,14 @@ let rec print_term info fmt t = with | Some s1, Some s2 -> if Term.ls_equal ls info.ls_rel_float.le + || Term.ls_equal ls info.ls_rel_float.lt || Term.ls_equal ls info.ls_rel_real.le + || Term.ls_equal ls info.ls_rel_real.lt then Fmt.pf fmt "+%s -%s <= 0" s1 s2 else if Term.ls_equal ls info.ls_rel_float.ge + || Term.ls_equal ls info.ls_rel_float.gt || Term.ls_equal ls info.ls_rel_real.ge + || Term.ls_equal ls info.ls_rel_real.gt then Fmt.pf fmt "+%s -%s >= 0" s1 s2 else Printer.unsupportedTerm t "Marabou: unknown relational operator" | _ -> Printer.unsupportedTerm t "Marabou: unknown variable(s)")