Skip to content

Commit

Permalink
Error using correct util and fix of documentation
Browse files Browse the repository at this point in the history
  • Loading branch information
Stevendeo committed Sep 26, 2023
1 parent 7cb0ac5 commit 99d4a8e
Show file tree
Hide file tree
Showing 3 changed files with 19 additions and 9 deletions.
5 changes: 2 additions & 3 deletions src/bin/common/solving_loop.ml
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ let empty_solver_ctx = {
}

let unsupported_opt s =
Printer.print_wrn "unsupported option %S" s
Printer.print_smtlib_err "unsupported option %S" s

let main () =
let () = Dolmen_loop.Code.init [] in
Expand Down Expand Up @@ -417,8 +417,7 @@ let main () =
let pp_reason_unknown fmt st =
let err () =
let msg = "Invalid (get-info :reason-unknown)" in
Printer.print_err "%s" msg;
Format.fprintf fmt "(error %S)" msg
Printer.fprint_smtlib_err fmt "%S" msg
in
match State.get partial_model_key st with
| None ->
Expand Down
11 changes: 8 additions & 3 deletions src/lib/util/printer.ml
Original file line number Diff line number Diff line change
Expand Up @@ -382,9 +382,7 @@ let print_status_preprocess ?(validity_mode=true)
("Preprocessing","","fg_magenta") None
time steps None

let print_smtlib_err ?(flushed=true) s =
(* The smtlib error messages are printed on the regular output. *)
let fmt = Options.Output.get_fmt_regular () in
let fprint_smtlib_err ?(flushed=true) fmt s =
let k fmt =
if flushed || Options.get_output_with_forced_flush () then
Format.fprintf fmt "\")@."
Expand All @@ -393,3 +391,10 @@ let print_smtlib_err ?(flushed=true) s =
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
12 changes: 9 additions & 3 deletions src/lib/util/printer.mli
Original file line number Diff line number Diff line change
Expand Up @@ -175,9 +175,15 @@ val print_status_preprocess :
float option ->
int option -> unit

(** Print smtlib error message on the error formatter accessible with
{!val:Options.get_fmt_err} and set by default to stderr.
The err formatter is flushed after the print if flushed is set *)
(** 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. *)
val print_smtlib_err :
?flushed:bool ->
('a, Format.formatter, unit) format -> 'a

0 comments on commit 99d4a8e

Please sign in to comment.