Model output is now const; this related to bug 519

2 files changed, 5 insertions, 3 deletions

diff --git a/src/util/util_model.cpp b/src/util/util_model.cpp
index ab4c95ea5..1c2dc2edf 100644
--- a/src/util/util_model.cpp
+++ b/src/util/util_model.cpp
@@ -24,7 +24,7 @@ using namespace std;
 
 namespace CVC4 {
 
-std::ostream& operator<<(std::ostream& out, Model& m) {
+std::ostream& operator<<(std::ostream& out, const Model& m) {
   smt::SmtScope smts(&m.d_smt);
   Expr::dag::Scope scope(out, false);
   Printer::getPrinter(options::outputLanguage())->toStream(out, m);
diff --git a/src/util/util_model.h b/src/util/util_model.h
index 535493a2d..365e7124d 100644
--- a/src/util/util_model.h
+++ b/src/util/util_model.h
@@ -29,10 +29,10 @@ class Command;
 class SmtEngine;
 class Model;
 
-std::ostream& operator<<(std::ostream&, Model&);
+std::ostream& operator<<(std::ostream&, const Model&);
 
 class Model {
-  friend std::ostream& operator<<(std::ostream&, Model&);
+  friend std::ostream& operator<<(std::ostream&, const Model&);
 
 protected:
   /** The SmtEngine we're associated with */
@@ -50,6 +50,8 @@ public:
   const Command* getCommand(size_t i) const;
   /** get the smt engine that this model is hooked up to */
   SmtEngine* getSmtEngine() { return &d_smt; }
+  /** get the smt engine (as a pointer-to-const) that this model is hooked up to */
+  const SmtEngine* getSmtEngine() const { return &d_smt; }
 
 public:
   /** get value for expression */