diff options
Diffstat (limited to 'src/smt/check_models.h')
-rw-r--r-- | src/smt/check_models.h | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/smt/check_models.h b/src/smt/check_models.h index 9b6780ddf..ce06bae07 100644 --- a/src/smt/check_models.h +++ b/src/smt/check_models.h @@ -22,10 +22,12 @@ #include "expr/node.h" namespace cvc5 { + +class Env; + namespace smt { class Model; -class SmtSolver; /** * This utility is responsible for checking the current model. @@ -33,7 +35,7 @@ class SmtSolver; class CheckModels { public: - CheckModels(SmtSolver& s); + CheckModels(Env& e); ~CheckModels(); /** * Check model m against the current set of input assertions al. @@ -44,8 +46,8 @@ class CheckModels void checkModel(Model* m, context::CDList<Node>* al, bool hardFailure); private: - /** Reference to the SMT solver */ - SmtSolver& d_smt; + /** Reference to the environment */ + Env& d_env; }; } // namespace smt |