From fbc56db7303c79f03f1028f2e7f66a874626e16b Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 20 Jun 2018 10:24:08 +0000
Subject: [PATCH] Remove unnecessarily inlined implementations to otherwise
 empty cpp file

---
 src/util/decision_procedure.cpp | 4 +++-
 src/util/decision_procedure.h   | 2 ++
 src/util/dstring.cpp            | 7 +++++++
 src/util/dstring.h              | 5 +----
 4 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/src/util/decision_procedure.cpp b/src/util/decision_procedure.cpp
index 132f1b0fc5c..d611fe7f24f 100644
--- a/src/util/decision_procedure.cpp
+++ b/src/util/decision_procedure.cpp
@@ -11,4 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "decision_procedure.h"
 
-
+decision_proceduret::~decision_proceduret()
+{
+}
diff --git a/src/util/decision_procedure.h b/src/util/decision_procedure.h
index b966cb96dd6..2def0b640a1 100644
--- a/src/util/decision_procedure.h
+++ b/src/util/decision_procedure.h
@@ -24,6 +24,8 @@ class decision_proceduret:public messaget
   {
   }
 
+  virtual ~decision_proceduret();
+
   // get a value from satisfying instance if satisfiable
   // returns nil if not available
   virtual exprt get(const exprt &expr) const=0;
diff --git a/src/util/dstring.cpp b/src/util/dstring.cpp
index 18602127ea1..b5a8847ff37 100644
--- a/src/util/dstring.cpp
+++ b/src/util/dstring.cpp
@@ -10,3 +10,10 @@ Author: Daniel Kroening, kroening@kroening.com
 /// Container for C-Strings
 
 #include "dstring.h"
+
+#include <ostream>
+
+std::ostream &dstringt::operator<<(std::ostream &out) const
+{
+  return out << as_string();
+}
diff --git a/src/util/dstring.h b/src/util/dstring.h
index 91c58a39f38..e0a98be9b20 100644
--- a/src/util/dstring.h
+++ b/src/util/dstring.h
@@ -123,10 +123,7 @@ class dstringt final
 
   // output
 
-  std::ostream &operator<<(std::ostream &out) const
-  {
-    return out << as_string();
-  }
+  std::ostream &operator<<(std::ostream &out) const;
 
   // non-standard