From 854dd1f3db6021af97a365e896e52e54fd9556f5 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 25 Sep 2023 15:45:38 +0200 Subject: [PATCH] Poetry --- src/bin/common/solving_loop.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index f68176fb5a..80956af1f6 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -417,12 +417,15 @@ 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 + the get-info. *) + 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 @@ -430,7 +433,7 @@ let main () = 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" ->