Making the ManagedOstream::defaultSource() a const function.

diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h
index 05d026b241a27accd4261c78f92db011a1eb8c8c..6dc7850273efc461a527a667516a6231cd0e0ba1 100644 (file)
--- a/src/smt/managed_ostreams.h
+++ b/src/smt/managed_ostreams.h
@@ -48,7 +48,7 @@ class ManagedOstream {
   void set(const std::string& filename);
 
   /** If this is associated with an option, return the string value. */
-  virtual std::string defaultSource() { return ""; }
+  virtual std::string defaultSource() const { return ""; }
 
  protected: