From 8cfc422b71d4ad26397267521bc80c86f1f1906c Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Tue, 26 Sep 2023 16:27:14 +0200 Subject: [PATCH] Better formatting to SMT lib --- src/bin/common/solving_loop.ml | 7 ++----- src/lib/reasoners/fun_sat.ml | 4 +--- 2 files changed, 3 insertions(+), 8 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 95465eca76..5de66f0a01 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -51,7 +51,7 @@ let empty_solver_ctx = { } let unsupported_opt s = - Printer.print_smtlib_err "unsupported option %S" s + Printer.print_std "(%s unsupported)" s let main () = let () = Dolmen_loop.Code.init [] in @@ -449,11 +449,8 @@ let main () = | ":all-statistics" | ":assertion-stack-levels" -> unsupported_opt kind; - print_std Fmt.string "unsupported" | _ -> - Printer.print_wrn "unknown option %S" kind; - print_std Fmt.string "unsupported" - + Printer.print_smtlib_err "unknown option %S" kind in let handle_stmt : diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 43e56a6a4c..dcd15881ac 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1394,9 +1394,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct with | Util.Not_implemented s -> Printer.print_err "Feature %s is not implemented. \ I can't conclude." s; - i_dont_know - "I stopped while trying to produce a model." - env + i_dont_know "incomplete" env (* should be merged with do_bcp/red/elim ? calls to debug hooks are missing *)