From 09ee60ccced6c419dee472b31ce75317a83485de Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Dec 2021 18:08:16 -0800 Subject: [PATCH] update comment Signed-off-by: Nikolaj Bjorner --- src/smt/smt_kernel.h | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 5c28d52fd..681bdd55b 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(); };