diff --git a/config/drivers/marabou.drv b/config/drivers/marabou.drv
index dafffbdb02f5a1c91127b7cb5f86a4bbc21345ab..2b23a906ee2e127043cc25f0f8c7d0bfcc24031b 100644
--- a/config/drivers/marabou.drv
+++ b/config/drivers/marabou.drv
@@ -117,9 +117,13 @@ theory real.Real
   meta "invalid trigger" predicate (>)
 
   syntax predicate (<=) "%1 <= %2"
-  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
   remove prop MulAssoc.Assoc
@@ -167,9 +171,13 @@ theory ieee_float.Float64
   syntax function (.-_) "(-%1)"
 
   syntax predicate le "%1 <= %2"
-  syntax predicate lt  "%1 <  %2"
   syntax predicate ge "%1 >= %2"
-  syntax predicate gt  "%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
 
 theory real.RealInfix
@@ -185,9 +193,13 @@ theory real.RealInfix
   meta "invalid trigger" predicate (>.)
 
   syntax predicate (<=.) "(%1 <= %2)"
-  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
 
 theory Bool
diff --git a/config/drivers/vnnlib.gen b/config/drivers/vnnlib.gen
index 5a2ae276cff87f3caf69ebe8cb0349acd27ebfc6..59c1c5d92e7c8dba640d4af0e1cefe31036a29f6 100644
--- a/config/drivers/vnnlib.gen
+++ b/config/drivers/vnnlib.gen
@@ -77,9 +77,13 @@ theory real.Real
   syntax function inv  "(/ 1.0 %1)"
 
   syntax predicate (<=) "(<= %1 %2)"
-  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
   meta "encoding:kept" type real
@@ -123,9 +127,13 @@ theory ieee_float.Float64
   syntax function (.-_) "(-%1)"
 
   syntax predicate le "(<= %1 %2)"
-  syntax predicate lt "(< %1 %2)"
   syntax predicate ge "(>= %1 %2)"
-  syntax predicate gt "(> %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 ""
   remove allprops
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
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
diff --git a/src/printers/vnnlib.ml b/src/printers/vnnlib.ml
index 2372b4d1174ea6257ada65ab42b2a18955b5aa8a..90888b432613d15d0ffcd05cdc5b2f7a00c10cee 100644
--- a/src/printers/vnnlib.ml
+++ b/src/printers/vnnlib.ml
@@ -445,20 +445,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
diff --git a/tests/interpretation_acasxu.t b/tests/interpretation_acasxu.t
index 2e04d6c537bfac608531692739c0e51de3a9a1e3..11080ff1a14afd138901ecd8cbbd46ca43c04037 100644
--- a/tests/interpretation_acasxu.t
+++ b/tests/interpretation_acasxu.t
@@ -4,7 +4,7 @@ Test interpret on acasxu
   $ bin/pyrat.py --version
   PyRAT 1.1
 
-  $ caisar verify --format whyml --prover PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
+  $ cat > file.mlw <<EOF
   > theory T
   >   use ieee_float.Float64
   >   use bool.Bool
@@ -92,6 +92,8 @@ Test interpret on acasxu
   >       not (advises nn i clear_of_conflict)
   > end
   > EOF
+
+  $ caisar verify --prover PyRAT --ltag=ProverSpec file.mlw 2>&1 | ./filter_tmpdir.sh
   [DEBUG]{ProverSpec} Prover-tailored specification:
   -0.328421367053318091766556108268559910356998443603515625 <= x0
   x0 <= 0.67985927880386987087746319957659579813480377197265625
@@ -130,3 +132,215 @@ Test interpret on acasxu
   
   Goal P1: Unknown ()
   Goal P3: Unknown ()
+
+  $ caisar verify --prover PyRAT --prover-altern VNNLIB --ltag=ProverSpec file.mlw 2>&1 | ./filter_tmpdir.sh
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  ;;; produced by PyRAT/VNN-LIB driver
+  ;;; produced by VNN-LIB driver
+  ;; X_0
+  (declare-const X_0 Real)
+  
+  ;; X_1
+  (declare-const X_1 Real)
+  
+  ;; X_2
+  (declare-const X_2 Real)
+  
+  ;; X_3
+  (declare-const X_3 Real)
+  
+  ;; X_4
+  (declare-const X_4 Real)
+  
+  ;; H
+  (assert (>= X_0 -0.328421367053318091766556108268559910356998443603515625))
+  
+  ;; H
+  (assert (<= X_0 0.67985927880386987087746319957659579813480377197265625))
+  
+  ;; H
+  (assert (>= X_1 -0.499999999999967081887319864108576439321041107177734375))
+  
+  ;; H
+  (assert (<= X_1 0.499999999999967081887319864108576439321041107177734375))
+  
+  ;; H
+  (assert (>= X_2 -0.499999999999967081887319864108576439321041107177734375))
+  
+  ;; H
+  (assert (<= X_2 0.499999999999967081887319864108576439321041107177734375))
+  
+  ;; H
+  (assert (>= X_3 -0.5))
+  
+  ;; H
+  (assert (<= X_3 0.5))
+  
+  ;; H
+  (assert (>= X_4 -0.5))
+  
+  ;; H
+  (assert (<= X_4 0.5))
+  
+  ;; H
+  (assert (>= X_0 0.60000151009774149724051994780893437564373016357421875))
+  
+  ;; H
+  (assert (>= X_3 0.450000000000000011102230246251565404236316680908203125))
+  
+  ;; H
+  (assert (<= X_4 -0.450000000000000011102230246251565404236316680908203125))
+  
+  ;; Y_0
+  (declare-const Y_0 Real)
+  
+  ;; Y_1
+  (declare-const Y_1 Real)
+  
+  ;; Y_2
+  (declare-const Y_2 Real)
+  
+  ;; Y_3
+  (declare-const Y_3 Real)
+  
+  ;; Y_4
+  (declare-const Y_4 Real)
+  
+  ;; Goal P1
+  (assert (>= Y_0 3.991125645861615112153231166303157806396484375))
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  ;;; produced by PyRAT/VNN-LIB driver
+  ;;; produced by VNN-LIB driver
+  ;; X_0
+  (declare-const X_0 Real)
+  
+  ;; X_1
+  (declare-const X_1 Real)
+  
+  ;; X_2
+  (declare-const X_2 Real)
+  
+  ;; X_3
+  (declare-const X_3 Real)
+  
+  ;; X_4
+  (declare-const X_4 Real)
+  
+  ;; H
+  (assert (>= X_0 -0.328421367053318091766556108268559910356998443603515625))
+  
+  ;; H
+  (assert (<= X_0 0.67985927880386987087746319957659579813480377197265625))
+  
+  ;; H
+  (assert (>= X_1 -0.499999999999967081887319864108576439321041107177734375))
+  
+  ;; H
+  (assert (<= X_1 0.499999999999967081887319864108576439321041107177734375))
+  
+  ;; H
+  (assert (>= X_2 -0.499999999999967081887319864108576439321041107177734375))
+  
+  ;; H
+  (assert (<= X_2 0.499999999999967081887319864108576439321041107177734375))
+  
+  ;; H
+  (assert (>= X_3 -0.5))
+  
+  ;; H
+  (assert (<= X_3 0.5))
+  
+  ;; H
+  (assert (>= X_4 -0.5))
+  
+  ;; H
+  (assert (<= X_4 0.5))
+  
+  ;; H
+  (assert (>= X_0 -0.303529646039727207806890874053351581096649169921875))
+  
+  ;; H
+  (assert (<= X_0 -0.298551301837009008810497334707179106771945953369140625))
+  
+  ;; H
+  (assert (>= X_1 -0.0095492965855130916563719978285007528029382228851318359375))
+  
+  ;; H
+  (assert (<= X_1 0.0095492965855130916563719978285007528029382228851318359375))
+  
+  ;; H
+  (assert (>= X_2 0.493380323584843072382000173092819750308990478515625))
+  
+  ;; H
+  (assert (>= X_3 0.299999999999999988897769753748434595763683319091796875))
+  
+  ;; H
+  (assert (>= X_4 0.299999999999999988897769753748434595763683319091796875))
+  
+  ;; Y_0
+  (declare-const Y_0 Real)
+  
+  ;; Y_1
+  (declare-const Y_1 Real)
+  
+  ;; Y_2
+  (declare-const Y_2 Real)
+  
+  ;; Y_3
+  (declare-const Y_3 Real)
+  
+  ;; Y_4
+  (declare-const Y_4 Real)
+  
+  ;; Goal P3
+  (assert (<= Y_0 Y_1))
+  (assert (<= Y_0 Y_2))
+  (assert (<= Y_0 Y_3))
+  (assert (<= Y_0 Y_4))
+  
+  Goal P1: Unknown ()
+  Goal P3: Unknown ()
+
+  $ caisar verify --prover Marabou --ltag=ProverSpec file.mlw 2>&1 | ./filter_tmpdir.sh
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= -0.328421367053318091766556108268559910356998443603515625
+  x0 <= 0.67985927880386987087746319957659579813480377197265625
+  x1 >= -0.499999999999967081887319864108576439321041107177734375
+  x1 <= 0.499999999999967081887319864108576439321041107177734375
+  x2 >= -0.499999999999967081887319864108576439321041107177734375
+  x2 <= 0.499999999999967081887319864108576439321041107177734375
+  x3 >= -0.5
+  x3 <= 0.5
+  x4 >= -0.5
+  x4 <= 0.5
+  x0 >= 0.60000151009774149724051994780893437564373016357421875
+  x3 >= 0.450000000000000011102230246251565404236316680908203125
+  x4 <= -0.450000000000000011102230246251565404236316680908203125
+  y0 >= 3.991125645861615112153231166303157806396484375
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= -0.328421367053318091766556108268559910356998443603515625
+  x0 <= 0.67985927880386987087746319957659579813480377197265625
+  x1 >= -0.499999999999967081887319864108576439321041107177734375
+  x1 <= 0.499999999999967081887319864108576439321041107177734375
+  x2 >= -0.499999999999967081887319864108576439321041107177734375
+  x2 <= 0.499999999999967081887319864108576439321041107177734375
+  x3 >= -0.5
+  x3 <= 0.5
+  x4 >= -0.5
+  x4 <= 0.5
+  x0 >= -0.303529646039727207806890874053351581096649169921875
+  x0 <= -0.298551301837009008810497334707179106771945953369140625
+  x1 >= -0.0095492965855130916563719978285007528029382228851318359375
+  x1 <= 0.0095492965855130916563719978285007528029382228851318359375
+  x2 >= 0.493380323584843072382000173092819750308990478515625
+  x3 >= 0.299999999999999988897769753748434595763683319091796875
+  x4 >= 0.299999999999999988897769753748434595763683319091796875
+  +y0 -y1 <= 0
+  +y0 -y2 <= 0
+  +y0 -y3 <= 0
+  +y0 -y4 <= 0
+  
+  Goal P1: Unknown ()
+  Goal P3: Unknown ()