diff --git a/config/drivers/marabou.drv b/config/drivers/marabou.drv
index 1f29308b6a1925b339ee08672f68183659a730d4..2b23a906ee2e127043cc25f0f8c7d0bfcc24031b 100644
--- a/config/drivers/marabou.drv
+++ b/config/drivers/marabou.drv
@@ -117,8 +117,12 @@ theory real.Real
   meta "invalid trigger" predicate (>)
 
   syntax predicate (<=) "%1 <= %2"
-  syntax predicate (<)  "%1 <= %2"
   syntax predicate (>=) "%1 >= %2"
+
+  (* Marabou supports only non-strict inequalities, hence we force strict
+     inequalities to be printed as non-strict ones.
+     This is not correct in general, and should be taken into account. *)
+  syntax predicate (<)  "%1 <= %2"
   syntax predicate (>)  "%1 >= %2"
 
   remove prop MulComm.Comm
@@ -167,8 +171,12 @@ theory ieee_float.Float64
   syntax function (.-_) "(-%1)"
 
   syntax predicate le "%1 <= %2"
-  syntax predicate lt "%1 <= %2"
   syntax predicate ge "%1 >= %2"
+
+  (* Marabou supports only non-strict inequalities, hence we force strict
+     inequalities to be printed as non-strict ones.
+     This is not correct in general, and should be taken into account. *)
+  syntax predicate lt "%1 <= %2"
   syntax predicate gt "%1 >= %2"
 end
 
@@ -185,8 +193,12 @@ theory real.RealInfix
   meta "invalid trigger" predicate (>.)
 
   syntax predicate (<=.) "(%1 <= %2)"
-  syntax predicate (<.)  "(%1 <= %2)"
   syntax predicate (>=.) "(%1 >= %2)"
+
+  (* Marabou supports only non-strict inequalities, hence we force strict
+     inequalities to be printed as non-strict ones.
+     This is not correct in general, and should be taken into account. *)
+  syntax predicate (<.)  "(%1 <= %2)"
   syntax predicate (>.)  "(%1 >= %2)"
 end
 
diff --git a/config/drivers/vnnlib.gen b/config/drivers/vnnlib.gen
index fe1bd19982e5579b0a641305b7b414e15acaa957..59c1c5d92e7c8dba640d4af0e1cefe31036a29f6 100644
--- a/config/drivers/vnnlib.gen
+++ b/config/drivers/vnnlib.gen
@@ -77,8 +77,12 @@ theory real.Real
   syntax function inv  "(/ 1.0 %1)"
 
   syntax predicate (<=) "(<= %1 %2)"
-  syntax predicate (<)  "(<= %1 %2)"
   syntax predicate (>=) "(>= %1 %2)"
+
+  (* VNN-LIB supports only non-strict inequalities, hence we force strict
+     inequalities to be printed as non-strict ones.
+     This is not correct in general, and should be taken into account. *)
+  syntax predicate (<)  "(<= %1 %2)"
   syntax predicate (>)  "(>= %1 %2)"
 
   remove allprops
@@ -123,8 +127,12 @@ theory ieee_float.Float64
   syntax function (.-_) "(-%1)"
 
   syntax predicate le "(<= %1 %2)"
-  syntax predicate lt "(<= %1 %2)"
   syntax predicate ge "(>= %1 %2)"
+
+  (* VNN-LIB supports only non-strict inequalities, hence we force strict
+     inequalities to be printed as non-strict ones.
+     This is not correct in general, and should be taken into account. *)
+  syntax predicate lt "(<= %1 %2)"
   syntax predicate gt "(>= %1 %2)"
 
   syntax predicate is_not_nan ""