From 5f91d0bd7694a3f7030486a7aa7a034175f11edc Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 27 Aug 2022 12:36:45 -0400
Subject: [PATCH] fix spurious \r

---
 src/main/main.ml      | 3 +--
 src/smtlib/Process.ml | 5 ++---
 2 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/src/main/main.ml b/src/main/main.ml
index 679e4d8d..a89c47f0 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -33,7 +33,6 @@ let p_progress = ref false
 let proof_file = ref ""
 let proof_store_memory = ref false
 let proof_store_file = ref ""
-let reset_line = "\x1b[2K\r"
 
 (* Arguments parsing *)
 let int_arg r arg =
@@ -184,7 +183,7 @@ let main_smt ~config () : _ result =
   in
 
   let finally () =
-    if !p_stat then Format.printf "%s%a@." reset_line Solver.pp_stats solver
+    if !p_stat then Format.printf "%a@." Solver.pp_stats solver
   in
   CCFun.protect ~finally @@ fun () ->
   (* FIXME: emit an actual proof *)
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index 1dea0d39..57f2b3f6 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -152,7 +152,7 @@ let solve ?gc:_ ?restarts:_ ?proof_file ?(pp_model = false) ?(check = false)
       Some (mk_progress s)
     else
       None
-  in
+  and clear_line () = if progress then Printf.printf "%s%!" reset_line in
 
   let should_stop =
     match time, memory with
@@ -181,7 +181,6 @@ let solve ?gc:_ ?restarts:_ ?proof_file ?(pp_model = false) ?(check = false)
     (* ?gc ?restarts ?time ?memory ?progress *)
   in
   let t2 = Sys.time () in
-  Printf.printf "\r";
   flush stdout;
   (match res with
   | Solver.Sat m ->
@@ -234,7 +233,7 @@ let solve ?gc:_ ?restarts:_ ?proof_file ?(pp_model = false) ?(check = false)
     Fmt.printf "unknown@.";
     Fmt.printf "; @[<h>:reason %a@]@." Solver.Unknown.pp reas
   | exception exn ->
-    Printf.printf "%s%!" reset_line;
+    clear_line ();
     raise exn);
   res