Escape quotes when printing SMT-LIB error messages (#1289)

* Escape quotes when printing SMT-LIB error messages

src/bin/common/solving_loop.ml

@@ -832,11 +832,11 @@ let process_source ?selector_inst ~print_status src =
       | {contents = `Exit; _} -> raise Exit
 
       | {contents = `Echo str; _} ->
-        let new_str = String.concat "\"\"" (String.split_on_char '"' str) in
         Fmt.pf
           (Options.Output.get_fmt_regular ())
-          "\"%s\"@."
-          new_str;
+          "%a@."
+          Printer.pp_smtlib_string
+          str;
         st
 
       | {contents = `Get_info kind; _ } ->

src/lib/util/printer.ml

@@ -375,6 +375,23 @@ let print_status_timeout ?(validity_mode=true) loc
     ("Timeout","unknown","fg_orange") loc
     time steps goal
 
+(* Version of [kfprintf] that escapes its input. *)
+let ekfprintf k ppf fmt =
+  let buf = Buffer.create 1024 in
+  let buf_ppf = Format.formatter_of_buffer buf in
+  Format.kfprintf (fun buf_ppf ->
+      Format.pp_print_flush buf_ppf ();
+      let s =
+        String.concat "\"\"" (String.split_on_char '"' (Buffer.contents buf))
+      in
+      Format.pp_print_string ppf s;
+      k ppf
+    ) buf_ppf fmt
+
+let pp_smtlib_string ppf s =
+  Format.fprintf ppf "\"";
+  ekfprintf (fun ppf -> Format.fprintf ppf "\"") ppf "%s" s
+
 let print_smtlib_err ?(flushed=true) s =
   (* The smtlib error messages are printed on the regular output. *)
   pp_std_smt ();
@@ -386,7 +403,7 @@ let print_smtlib_err ?(flushed=true) s =
       Format.fprintf fmt "\")"
   in
   Format.fprintf fmt "(error \"";
-  Format.kfprintf k fmt s
+  ekfprintf k fmt s
 
 let pp_source ppf src =
   let name = Logs.Src.doc src in

src/lib/util/printer.mli

@@ -161,6 +161,9 @@ val print_status_inconsistent :
   int option ->
   string option -> unit
 
+(** Print an SMT-LIB string with quotes and escaping. *)
+val pp_smtlib_string : Format.formatter -> string -> unit
+
 (** Print smtlib error message on the regular formatter, accessible with
     {!val:Options.get_fmt_regular} and set by default to stdout.
     The regular formatter is flushed after the print if flushed is set. *)

tests/smtlib/testfile-get-assignment1.err.expected

@@ -1,2 +1,2 @@
 (error "../tests/smtlib/testfile-get-assignment1.err.smt2:3.0:
-        No model produced, cannot execute get-assignment.")
+No model produced, cannot execute get-assignment.")

tests/smtlib/testfile-get-assignment2.err.expected

@@ -4,4 +4,4 @@ unknown
   (define-fun x () Int 0)
 )
 (error "../tests/smtlib/testfile-get-assignment2.err.smt2:8.0:
-        Produce assignments disabled; add (set-option :produce-assignments true)")
+Produce assignments disabled; add (set-option :produce-assignments true)")

tests/smtlib/testfile-get-info2.err.expected

@@ -1,2 +1,2 @@
 (error "../tests/smtlib/testfile-get-info2.err.smt2:7.0:
-        Invalid (get-info :reason-unknown)")
+Invalid (get-info :reason-unknown)")