diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index d153284314..b69d7265c9 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -32,22 +32,6 @@ open Commands open Format open Options -let timeout_reason_to_string = function - | Sat_solver_sig.Assume -> "Assume" - | ProofSearch -> "ProofSearch" - | ModelGen -> "ModelGen" - -let unknown_reason_to_string = function - | Sat_solver_sig.Incomplete -> "Incomplete" - | Memout -> "Memout" - | Steps_limit n -> Fmt.str "Step limit reached: %i" n - | Timeout t -> Fmt.str "Timeout:%s" (timeout_reason_to_string t) - -let unknown_reason_opt_to_string = - function - | None -> "Decided" - | Some r -> unknown_reason_to_string r - module E = Expr module Ex = Explanation diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index 99b0ccc838..a276f6568f 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -42,11 +42,7 @@ type unknown_reason = | Memout | Steps_limit of int | Timeout of timeout_reason - -let pp_unknown_reason ppf = function - | Incomplete -> Fmt.pf ppf "Incomplete" - | Memout -> Fmt.pf ppf "Memout" - | Timeout t -> Fmt.pf ppf "Timeout:%a" pp_timeout_reason t +[@@deriving show] let pp_unknown_reason_opt ppf = function | None -> Fmt.pf ppf "Decided"