diff --git a/config/drivers/pyrat.drv b/config/drivers/pyrat.drv
index ddf120e7dee37f38d1a4b712a2153fb4a5704d06..77dff7e0bd0288d0a4ab62586106a45086abee76 100644
--- a/config/drivers/pyrat.drv
+++ b/config/drivers/pyrat.drv
@@ -1,6 +1,6 @@
 (* Why3 drivers for PyRAT *)
 
-prelude "(* this is the prelude for PyRAT *)"
+prelude "(* This is the prelude for PyRAT *)"
 
 (* additional regexp for detection of answers, needed for alt-ergo <= 0.99 *)
 valid "^Inconsistent assumption$"
diff --git a/src/language.mli b/src/language.mli
index f1812f1d3e175236b0ffaa112cf1eeb77088284b..71482631586333d265b079a0901af77bc8545369 100644
--- a/src/language.mli
+++ b/src/language.mli
@@ -12,7 +12,7 @@ type nnet = {
 }
 
 val lookup_loaded_nnets : Why3.Term.lsymbol -> nnet option
-(** @return the filename of an nnets Why3 representation. *)
+(** @return the filename of a nnet Why3 representation. *)
 
 val register_nnet_support : unit -> unit
 (** Register nnet parser. *)
diff --git a/src/printer/pyrat.ml b/src/printer/pyrat.ml
index e0471186ebece8418a828550c6d95a3c7dcbfcaa..a852b9cd1cc8366ffbaa1d70c6ab62768a917773 100644
--- a/src/printer/pyrat.ml
+++ b/src/printer/pyrat.ml
@@ -29,7 +29,7 @@ let rec print_term info fmt t =
   | Tbinop ((Timplies | Tiff), _, _)
   | Tnot _ | Ttrue | Tfalse | Tvar _ | Tlet _ | Tif _ | Tcase _ | Tquant _
   | Teps _ ->
-    Printer.unsupportedTerm t "Pyrat"
+    Printer.unsupportedTerm t "Not supported by PyRAT"
   | Tbinop (Tand, _, _) -> assert false (* Should appear only at top-level. *)
   | Tconst c -> Constant.(print number_format unsupported_escape) fmt c
   | Tapp (ls, l) -> (
@@ -42,7 +42,7 @@ let rec print_term info fmt t =
   | Tbinop (Tor, t1, t2) ->
     Fmt.pf fmt "%a or %a" (print_term info) t1 (print_term info) t2
 
-let print_top_level_term info fmt t =
+let rec print_top_level_term info fmt t =
   let open Why3 in
   (* Don't print things we don't know. *)
   let t_is_known =
@@ -55,7 +55,12 @@ let print_top_level_term info fmt t =
   | Tquant _ -> ()
   | Tbinop (Tand, t1, t2) ->
     if t_is_known t1 && t_is_known t2
-    then Fmt.pf fmt "%a@.%a" (print_term info) t1 (print_term info) t2
+    then
+      Fmt.pf fmt "%a%a"
+        (print_top_level_term info)
+        t1
+        (print_top_level_term info)
+        t2
   | _ -> if t_is_known t then Fmt.pf fmt "%a@." (print_term info) t
 
 let print_decl info fmt d =
diff --git a/tests/simple.t b/tests/simple.t
index f01724c99a5066e5fe3d3c92418310b3c2ddcfe0..18ca8bf18626996a9fe554df37edb5a84790cbde 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -39,6 +39,11 @@ Test verify
   >      (0.0:t) .< x1 .< (0.5:t) ->
   >      let (y1,_,_,_,_) = nnet_apply x1 x2 x3 x4 x5 in
   >      (0.0:t) .< y1 .< (0.5:t)
+  > 
+  >   goal H: forall x1 x2 x3 x4 x5.
+  >      (0.0:t) .< x1 .< (0.5:t) /\ (0.5:t) .< x2 .< (1.0:t) ->
+  >      let (y1,y2,_,_,_) = nnet_apply x1 x2 x3 x4 x5 in
+  >      ((0.0:t) .< y1 \/ (0.5:t) .< y1) /\ (0.0:t) .< y2 .< (0.5:t)
   > end
   > EOF
   <autodetect>0 prover(s) added
@@ -54,8 +59,16 @@ Test verify
   <autodetect>Found prover Marabou version 1.0.+, OK.
   <autodetect>Found prover PyRAT version 1.0, OK.
   <autodetect>3 prover(s) added
-  (* this is the prelude for PyRAT *)
+  (* This is the prelude for PyRAT *)
   0.0 <  x0
   x0 <  0.5
   0.0 <  y0
   y0 <  0.5
+  (* This is the prelude for PyRAT *)
+  0.0 <  x0
+  x0 <  0.5
+  0.5 <  x1
+  x1 <  1.0
+  0.0 <  y0 or 0.5 <  y0
+  0.0 <  y1
+  y1 <  0.5