5 files changed, 20 insertions, 9 deletions
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 18ecbc316..574a57f19 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -820,7 +820,18 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) {
   // can only output datatypes in the CVC4 native language
   Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4);
 
-  os << "DATATYPE " << dt.getName() << " =" << endl;
+  os << "DATATYPE " << dt.getName();
+  if(dt.isParametric()) {
+    os << '[';
+    for(size_t i = 0; i < dt.getNumParameters(); ++i) {
+      if(i > 0) {
+        os << ',';
+      }
+      os << dt.getParameter(i);
+    }
+    os << ']';
+  }
+  os << " =" << endl;
   Datatype::const_iterator i = dt.begin(), i_end = dt.end();
   if(i != i_end) {
     os << "  ";
diff --git a/src/util/datatype.h b/src/util/datatype.h
index de38d8835..4b6894ef8 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -450,7 +450,7 @@ public:
    * Create a new Datatype of the given name, with the given
    * parameterization.
    */
-  inline Datatype(std::string name, std::vector<Type>& params);
+  inline Datatype(std::string name, const std::vector<Type>& params);
 
   /**
    * Add a constructor to this Datatype.  Constructor names need not
@@ -620,7 +620,7 @@ inline Datatype::Datatype(std::string name) :
   d_self() {
 }
 
-inline Datatype::Datatype(std::string name, std::vector<Type>& params) :
+inline Datatype::Datatype(std::string name, const std::vector<Type>& params) :
   d_name(name),
   d_params(params),
   d_constructors(),
diff --git a/src/util/dense_map.h b/src/util/dense_map.h
index 222a761c3..b7d690811 100644
--- a/src/util/dense_map.h
+++ b/src/util/dense_map.h
@@ -98,7 +98,7 @@ public:
       return false;
     }else{
       Assert(x <  allocated());
-      return d_posVector[x] != POSITION_SENTINEL;
+      return d_posVector[x] != +POSITION_SENTINEL;
     }
   }
 
@@ -160,7 +160,7 @@ public:
   void pop_back() {
     Assert(!empty());
     Key atBack = back();
-    d_posVector[atBack] = POSITION_SENTINEL;
+    d_posVector[atBack] = +POSITION_SENTINEL;
     d_image[atBack] = T();
     d_list.pop_back();
   }
@@ -195,7 +195,7 @@ public:
 
   void increaseSize(Key max){
     Assert(max >= allocated());
-    d_posVector.resize(max+1, POSITION_SENTINEL);
+    d_posVector.resize(max+1, +POSITION_SENTINEL);
     d_image.resize(max+1);
   }
 
diff --git a/src/util/hash.h b/src/util/hash.h
index 4d4094143..913358512 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -48,7 +48,7 @@ namespace CVC4 {
 
 struct StringHashFunction {
   size_t operator()(const std::string& str) const {
-    return std::hash<const char*>()(str.c_str());
+    return __gnu_cxx::hash<const char*>()(str.c_str());
   }
 };/* struct StringHashFunction */
 
diff --git a/src/util/statistics.i b/src/util/statistics.i
index 74cee5f37..7f3bbe526 100644
--- a/src/util/statistics.i
+++ b/src/util/statistics.i
@@ -4,7 +4,7 @@
 #ifdef SWIGJAVA
 
 #include "bindings/java_iterator_adapter.h"
-#include "bindings/java_output_stream_adapter.h"
+#include "bindings/java_stream_adapters.h"
 
 #endif /* SWIGJAVA */
 %}
@@ -72,7 +72,7 @@
 #ifdef SWIGJAVA
 
 %include "bindings/java_iterator_adapter.h"
-%include "bindings/java_output_stream_adapter.h"
+%include "bindings/java_stream_adapters.h"
 
 %template(JavaIteratorAdapter_StatisticsBase) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>;