SmtEngine::getModel() is now public. (#1665)

1 files changed, 7 insertions, 9 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 377888a5a..83300afc9 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -387,8 +387,6 @@ class CVC4_PUBLIC SmtEngine {
   // to access d_modelCommands
   friend class ::CVC4::Model;
   friend class ::CVC4::theory::TheoryModel;
-  // to access getModel(), which is private (for now)
-  friend class GetModelCommand;
 
   StatisticsRegistry* d_statisticsRegistry;
 
@@ -403,13 +401,6 @@ class CVC4_PUBLIC SmtEngine {
    */
   void addToModelCommandAndDump(const Command& c, uint32_t flags = 0, bool userVisible = true, const char* dumpTag = "declarations");
 
-  /**
-   * Get the model (only if immediately preceded by a SAT
-   * or INVALID query).  Only permitted if CVC4 was built with model
-   * support and produce-models is on.
-   */
-  Model* getModel();
-
   // disallow copy/assignment
   SmtEngine(const SmtEngine&) CVC4_UNDEFINED;
   SmtEngine& operator=(const SmtEngine&) CVC4_UNDEFINED;
@@ -489,6 +480,13 @@ class CVC4_PUBLIC SmtEngine {
       /* throw(OptionException, ModalException) */;
 
   /**
+   * Get the model (only if immediately preceded by a SAT
+   * or INVALID query).  Only permitted if CVC4 was built with model
+   * support and produce-models is on.
+   */
+  Model* getModel();
+
+  /**
    * Get an aspect of the current SMT execution environment.
    */
   CVC4::SExpr getOption(const std::string& key) const