diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index c44842474a8..a94dd842cf5 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -82,26 +82,13 @@ solver_factoryt::solvert::stack_decision_procedure() const } void solver_factoryt::set_decision_procedure_time_limit( - decision_proceduret &decision_procedure) + solver_resource_limitst &decision_procedure) { const int timeout_seconds = options.get_signed_int_option("solver-time-limit"); if(timeout_seconds > 0) - { - solver_resource_limitst *solver = - dynamic_cast(&decision_procedure); - if(solver == nullptr) - { - messaget log(message_handler); - log.warning() << "cannot set solver time limit on " - << decision_procedure.decision_procedure_text() - << messaget::eom; - return; - } - - solver->set_time_limit_seconds(timeout_seconds); - } + decision_procedure.set_time_limit_seconds(timeout_seconds); } void solver_factoryt::solvert::set_decision_procedure( @@ -531,7 +518,6 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver) if(options.get_bool_option("fpa")) smt2_dec->use_FPA_theory = true; - set_decision_procedure_time_limit(*smt2_dec); return std::make_unique(std::move(smt2_dec)); } else if(filename == "-") @@ -547,7 +533,6 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver) if(options.get_bool_option("fpa")) smt2_conv->use_FPA_theory = true; - set_decision_procedure_time_limit(*smt2_conv); return std::make_unique(std::move(smt2_conv)); } else @@ -565,7 +550,6 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver) if(options.get_bool_option("fpa")) smt2_conv->use_FPA_theory = true; - set_decision_procedure_time_limit(*smt2_conv); return std::make_unique(std::move(smt2_conv), std::move(out)); } } diff --git a/src/goto-checker/solver_factory.h b/src/goto-checker/solver_factory.h index c172e9bd2ec..8ebeb2a4638 100644 --- a/src/goto-checker/solver_factory.h +++ b/src/goto-checker/solver_factory.h @@ -21,6 +21,7 @@ class cmdlinet; class message_handlert; class namespacet; class optionst; +class solver_resource_limitst; class stack_decision_proceduret; class solver_factoryt final @@ -81,8 +82,8 @@ class solver_factoryt final /// Sets the timeout of \p decision_procedure if the `solver-time-limit` /// option has a positive value (in seconds). /// \note Most solvers silently ignore the time limit at the moment. - void - set_decision_procedure_time_limit(decision_proceduret &decision_procedure); + void set_decision_procedure_time_limit( + solver_resource_limitst &decision_procedure); // consistency checks during solver creation void no_beautification();