diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 5c28d52fd64..681bdd55b8f 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -307,13 +307,13 @@ namespace smt { /** \brief Return a reference to smt::context. - This is a temporary hack to support user theories. - TODO: remove this hack. - We need to revamp user theories too. + This breaks abstractions. + + It is currently used by the opt-solver + to access optimization services from arithmetic solvers + and to ensure that the solver has registered PB theory solver. - This method breaks the abstraction barrier. - - \warning We should not use this method + \warning This method should not be used in new code. */ context & get_context(); };