From c159fa2605417d0ad04a0a4e8ab849323b6fd071 Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Fri, 14 Jul 2017 16:07:38 +0100
Subject: [PATCH] Make message::get_mstream const

Changes message::mstream object to mutable so that message::debug()
and its friends can be run by constant methods.

Warning: in the future, when implementing multiple threads,
implementation of get_mstream will have to be changed so that each
thread has its own, local standard output. As it stands each
get_mstream() call changes stream type for the whole program.
---
 src/util/message.h | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/util/message.h b/src/util/message.h
index 230a795937c..9da886b0404 100644
--- a/src/util/message.h
+++ b/src/util/message.h
@@ -236,50 +236,50 @@ class messaget
     return m;
   }
 
-  mstreamt &get_mstream(unsigned message_level)
+  mstreamt &get_mstream(unsigned message_level) const
   {
     mstream.message_level=message_level;
     return mstream;
   }
 
-  mstreamt &error()
+  mstreamt &error() const
   {
     return get_mstream(M_ERROR);
   }
 
-  mstreamt &warning()
+  mstreamt &warning() const
   {
     return get_mstream(M_WARNING);
   }
 
-  mstreamt &result()
+  mstreamt &result() const
   {
     return get_mstream(M_RESULT);
   }
 
-  mstreamt &status()
+  mstreamt &status() const
   {
     return get_mstream(M_STATUS);
   }
 
-  mstreamt &statistics()
+  mstreamt &statistics() const
   {
     return get_mstream(M_STATISTICS);
   }
 
-  mstreamt &progress()
+  mstreamt &progress() const
   {
     return get_mstream(M_PROGRESS);
   }
 
-  mstreamt &debug()
+  mstreamt &debug() const
   {
     return get_mstream(M_DEBUG);
   }
 
 protected:
   message_handlert *message_handler;
-  mstreamt mstream;
+  mutable mstreamt mstream;
 };
 
 #endif // CPROVER_UTIL_MESSAGE_H