Fix Java output stream adapter.

diff --git a/src/bindings/java_stream_adapters.h b/src/bindings/java_stream_adapters.h
index eefb31e6d5f8be3f159a3eb1bbac1bfccf00c923..f3546613c20baf2c5f4cf8dd0a0428e676b50ba8 100644 (file)
--- a/src/bindings/java_stream_adapters.h
+++ b/src/bindings/java_stream_adapters.h
@@ -42,14 +42,9 @@
 
 namespace CVC4 {
 
-class JavaOutputStreamAdapter {
-  std::stringstream d_ss;
-
+class JavaOutputStreamAdapter : public std::ostringstream {
 public:
-  JavaOutputStreamAdapter() { }
-
-  std::string toString() { return d_ss.str(); }
-
+  std::string toString() { return str(); }
 };/* class JavaOutputStreamAdapter */
 
 class JavaInputStreamAdapter : public std::stringstream {