Better formatting to SMT lib

Stevendeo · Sep 26, 2023 · 8cfc422 · 8cfc422
1 parent 99d4a8e
commit 8cfc422
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 8 deletions.
diff --git 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
@@ -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 *)