From 6a9a63e2368c59a10b2e00d6cca2c44ed604dfe4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <129742207+bclement-ocp@users.noreply.github.com> Date: Mon, 10 Jul 2023 09:50:19 +0000 Subject: [PATCH] Display "timeout" result even if timeout occurs in model generation (#722) Fixes #704 Note that this doesn't really fix the issue with smtlib2 tests/arith/testfile-arith028.ae because we display "timeout" instead of "unknown", but at least we respect the output format now. --- src/lib/frontend/frontend.ml | 16 +++++----------- src/lib/reasoners/fun_sat.ml | 8 ++++---- 2 files changed, 9 insertions(+), 15 deletions(-) diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index e917d398c..5b7c4b02a 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -313,19 +313,13 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct (Some loc) (Some time) (Some steps) (get_goal_name d); | Timeout (Some d) -> - if Options.get_interpretation () then - Printer.print_wrn "Timeout" - else - let loc = d.st_loc in - Printer.print_status_timeout ~validity_mode - (Some loc) (Some time) (Some steps) (get_goal_name d); + let loc = d.st_loc in + Printer.print_status_timeout ~validity_mode + (Some loc) (Some time) (Some steps) (get_goal_name d); | Timeout None -> - if Options.get_interpretation () then - Printer.print_wrn "Timeout" - else - Printer.print_status_timeout ~validity_mode - None (Some time) (Some steps) None; + Printer.print_status_timeout ~validity_mode + None (Some time) (Some steps) None; | Preprocess -> Printer.print_status_preprocess ~validity_mode diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 586dff137..35ae79b0e 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1164,14 +1164,14 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct begin match !latest_saved_env with | None -> - Printer.print_fmt (Options.Output.get_fmt_std ()) - "@[[FunSat]@, \ + Printer.print_wrn + "[FunSat]@, @[\ It seems that no model has been computed so far.@,\ You may need to change your model generation strategy@,\ or to increase your timeout.@]" | Some env -> - Printer.print_fmt (Options.Output.get_fmt_std ()) - "@[[FunSat]@, \ + Printer.print_wrn + "[FunSat]@, @[\ A model has been computed. However, I failed \ while computing it so may be incorrect.@]"; let prop_model = extract_prop_model ~complete_model:true env in