diff --git a/config/drivers/marabou.drv b/config/drivers/marabou.drv
index dafffbdb02f5a1c91127b7cb5f86a4bbc21345ab..1f29308b6a1925b339ee08672f68183659a730d4 100644
--- a/config/drivers/marabou.drv
+++ b/config/drivers/marabou.drv
@@ -117,9 +117,9 @@ theory real.Real
   meta "invalid trigger" predicate (>)
 
   syntax predicate (<=) "%1 <= %2"
-  syntax predicate (<)  "%1 < %2"
+  syntax predicate (<)  "%1 <= %2"
   syntax predicate (>=) "%1 >= %2"
-  syntax predicate (>)  "%1 > %2"
+  syntax predicate (>)  "%1 >= %2"
 
   remove prop MulComm.Comm
   remove prop MulAssoc.Assoc
@@ -167,9 +167,9 @@ theory ieee_float.Float64
   syntax function (.-_) "(-%1)"
 
   syntax predicate le "%1 <= %2"
-  syntax predicate lt  "%1 <  %2"
+  syntax predicate lt "%1 <= %2"
   syntax predicate ge "%1 >= %2"
-  syntax predicate gt  "%1 >  %2"
+  syntax predicate gt "%1 >= %2"
 end
 
 theory real.RealInfix
@@ -185,9 +185,9 @@ theory real.RealInfix
   meta "invalid trigger" predicate (>.)
 
   syntax predicate (<=.) "(%1 <= %2)"
-  syntax predicate (<.)  "(%1 <  %2)"
+  syntax predicate (<.)  "(%1 <= %2)"
   syntax predicate (>=.) "(%1 >= %2)"
-  syntax predicate (>.)  "(%1 >  %2)"
+  syntax predicate (>.)  "(%1 >= %2)"
 end
 
 theory Bool
diff --git a/src/printers/marabou.ml b/src/printers/marabou.ml
index 5b888e204bb844ab4006f31418c6d3f6bfa6a4c1..fe887fb263cfefae6fbd1eefaf5b148006e02d97 100644
--- a/src/printers/marabou.ml
+++ b/src/printers/marabou.ml
@@ -128,20 +128,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