Poetry

src/bin/common/solving_loop.ml

@@ -417,20 +417,23 @@ let main () =
   let pp_reason_unknown fmt st =
     match State.get partial_model_key st with
     | None ->
-      (* This case should not happen. *)
-      Format.fprintf fmt "--"
+      (* This case should happen only when there is no check-sat before
+         a get-info statement. *)
+      Printer.print_err "Invalid (get-info :reason-unknown)";
+      Format.fprintf fmt ""
     | Some sat ->
       match SAT.get_unknown_reason sat with
       | None ->
-        Format.fprintf fmt "solver did not respond unknown"
+        Printer.print_err "Invalid (get-info :reason-unknown)";
+        Format.fprintf fmt ""
       | Some s ->
         Format.pp_print_string fmt s
   in
 
   let handle_get_info (st : State.t) (kind: string) =
     let print_std =
       fun (type a) (pp :(Format.formatter -> a -> unit)) (a : a) ->
-        Printer.print_std "(%s %a)" kind pp a
+        Printer.print_std "(%s \"%a\")" kind pp a
     in
     match kind with
     | ":authors" ->