From dc607b21b69110b7a8d00dd60016bf44bca27386 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 19 Jul 2023 13:56:00 +0200 Subject: [PATCH] Revert "Fix the error message." This reverts commit 27c220a1b4eee4c981597095516fdb4de939dbca. --- src/bin/common/solving_loop.ml | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 05b86b213..1316438a1 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -363,9 +363,9 @@ let main () = if Stdlib.(Options.get_sat_solver () = Tableaux) then Options.set_interpretation ILast else Printer.print_wrn "%a The generation of models is not supported \ - for the SAT solver %a. Please choose the \ + for the current SAT solver. Please choose the \ SAT solver Tableaux." - Loc.report st_loc Util.pp_sat_solver (Options.get_sat_solver ()) + Loc.report st_loc | ":produce-models", Symbol { name = Simple "false"; _ } -> Options.set_interpretation INone | ":produce-unsat-cores", Symbol { name = Simple "true"; _ } -> @@ -519,14 +519,6 @@ let main () = (* TODO: add the location of the statement. *) Printer.print_smtlib_err "No model produced."; st - else if Stdlib.(Options.get_sat_solver () <> Tableaux) then - begin - (* TODO: add the location of the statement. *) - Printer.print_smtlib_err - "get-model is not supported with the SAT solver %a." - Util.pp_sat_solver (Options.get_sat_solver ()); - st - end else begin (* TODO: add the location of the statement. *)