Fixing formatting & adding test

src/bin/common/solving_loop.ml

@@ -414,43 +414,39 @@ let main () =
     | _ -> unsupported_opt name
   in
 
-  let pp_reason_unknown fmt st =
-    let err () =
-      let msg = "Invalid (get-info :reason-unknown)" in
-      Printer.fprint_smtlib_err fmt "%S" msg
-    in
-    match State.get partial_model_key st with
-    | None ->
-      (* This case should happen only when there is no check-sat before
-         a get-info statement. *)
-      err ()
-    | Some sat ->
-      match SAT.get_unknown_reason sat with
-      | None -> err ()
-      | 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 :a Fmt.t) (a : a) ->
         Printer.print_std "(%s %a)" kind pp a
     in
+    let pp_reason_unknown st =
+      let err () =
+        let msg = "Invalid (get-info :reason-unknown)" in
+        Printer.print_smtlib_err "%s" msg
+      in
+      match State.get partial_model_key st with
+      | None -> err ()
+      | Some sat ->
+        match SAT.get_unknown_reason sat with
+        | None -> err ()
+        | Some s -> print_std Format.pp_print_string s
+    in
     match kind with
     | ":authors" ->
       print_std (fun fmt -> Fmt.pf fmt "%S") "Alt-Ergo developers"
     | ":error-behavior" ->
       print_std Fmt.string "immediate-exit"
     | ":name" ->
-      print_std (fun fmt -> Fmt.pf fmt "%S") "alt-ergo"
+      print_std (fun fmt -> Fmt.pf fmt "%S") "Alt-Ergo"
     | ":reason-unknown" ->
-      print_std pp_reason_unknown st
+      pp_reason_unknown st
     | ":version" ->
       print_std Fmt.string Version._version
     | ":all-statistics"
     | ":assertion-stack-levels" ->
       unsupported_opt kind;
     | _ ->
-      Printer.print_smtlib_err "unknown option %S" kind
+      Printer.print_smtlib_err "unknown option '%s'" kind
   in
 
   let handle_stmt :

src/lib/util/printer.ml

@@ -382,19 +382,14 @@ let print_status_preprocess ?(validity_mode=true)
     ("Preprocessing","","fg_magenta") None
     time steps None
 
-let fprint_smtlib_err ?(flushed=true) fmt s =
+let print_smtlib_err ?(flushed=true) s =
   let k fmt =
     if flushed || Options.get_output_with_forced_flush () then
       Format.fprintf fmt "\")@."
     else
       Format.fprintf fmt "\")"
   in
+  (* The smtlib error messages are printed on the regular output. *)
+  let fmt = (Options.Output.get_fmt_regular ()) in
   Format.fprintf fmt "(error \"";
   Format.kfprintf k fmt s
-
-let print_smtlib_err ?(flushed=true) s =
-  (* The smtlib error messages are printed on the regular output. *)
-  fprint_smtlib_err
-    ~flushed
-    (Options.Output.get_fmt_regular ())
-    s

src/lib/util/printer.mli

@@ -175,12 +175,6 @@ val print_status_preprocess :
   float option ->
   int option -> unit
 
-(** Print smtlib error message on the formatter in argument. *)
-val fprint_smtlib_err :
-  ?flushed:bool ->
-  Format.formatter ->
-  ('a, Format.formatter, unit) format -> 'a
-
 (** 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/everything/testfile-smt-instr-get-info.dolmen.expected

@@ -0,0 +1,11 @@
+(error "Invalid (get-info :reason-unknown)")
+
+unsat
+(:all-statistics unsupported)
+(:assertion-stack-levels unsupported)
+(:authors "Alt-Ergo developers")
+(:error-behavior immediate-exit)
+(:name "Alt-Ergo")
+(error "Invalid (get-info :reason-unknown)")
+(:version dev)
+(error "unknown option ':foo'")

tests/everything/testfile-smt-instr-get-info.dolmen.smt2

@@ -0,0 +1,16 @@
+(set-logic ALL)
+
+(declare-const x Int)
+(declare-const y Int)
+(assert (= (* x x) 3))
+
+(get-info :reason-unknown)
+(check-sat)
+(get-info :all-statistics)
+(get-info :assertion-stack-levels)
+(get-info :authors)
+(get-info :error-behavior)
+(get-info :name)
+(get-info :reason-unknown)
+(get-info :version)
+(get-info :foo)