2 files changed, 110 insertions, 0 deletions
diff --git a/nixpkgs/pkgs/applications/science/logic/cvc3/cvc3-2.4.1-gccv6-fix.patch b/nixpkgs/pkgs/applications/science/logic/cvc3/cvc3-2.4.1-gccv6-fix.patch
new file mode 100644
index 000000000000..1fb3516b8c27
--- /dev/null
+++ b/nixpkgs/pkgs/applications/science/logic/cvc3/cvc3-2.4.1-gccv6-fix.patch
@@ -0,0 +1,76 @@
+commit 4eb28b907e89be05d92eb704115f821b9b848e60
+Author: Matthew Dawson <matthew@mjdsystems.ca>
+Date:   Sun Oct 16 22:06:03 2016 -0400
+
+    Fix gcc v6 compile failures.
+    
+     * Use std::hash<const char*> over std::hash<char *>, as throwing away the const is not allowed.
+     * Use Hash::hash by default in CDMap over std::hash, to get Hash::hash<CVC3::expr>
+
+diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp
+index 0c85ff6..e4dd251 100644
+--- a/src/expr/expr_value.cpp
++++ b/src/expr/expr_value.cpp
+@@ -29,7 +29,7 @@ namespace CVC3 {
+ // Class ExprValue static members
+ ////////////////////////////////////////////////////////////////////////
+ 
+-std::hash<char*> ExprValue::s_charHash;
++std::hash<const char*> ExprValue::s_charHash;
+ std::hash<long int> ExprValue::s_intHash;
+ 
+ ////////////////////////////////////////////////////////////////////////
+diff --git a/src/include/cdmap.h b/src/include/cdmap.h
+index faf682a..c3b094c 100644
+--- a/src/include/cdmap.h
++++ b/src/include/cdmap.h
+@@ -43,9 +43,9 @@ namespace CVC3 {
+ // Auxiliary class: almost the same as CDO (see cdo.h), but on
+ // setNull() call it erases itself from the map.
+ 
+-template <class Key, class Data, class HashFcn = std::hash<Key> > class CDMap;
++template <class Key, class Data, class HashFcn = Hash::hash<Key> > class CDMap;
+ 
+-template <class Key, class Data, class HashFcn = std::hash<Key> >
++template <class Key, class Data, class HashFcn = Hash::hash<Key> >
+ class CDOmap :public ContextObj {
+   Key d_key;
+   Data d_data;
+diff --git a/src/include/expr_hash.h b/src/include/expr_hash.h
+index b2107d7..baa2eab 100644
+--- a/src/include/expr_hash.h
++++ b/src/include/expr_hash.h
+@@ -20,7 +20,6 @@
+  * hash_set over Expr class.
+  */
+ /*****************************************************************************/
+-
+ #ifndef _cvc3__expr_h_
+ #include "expr.h"
+ #endif
+diff --git a/src/include/expr_value.h b/src/include/expr_value.h
+index 95102b2..f53aa4d 100644
+--- a/src/include/expr_value.h
++++ b/src/include/expr_value.h
+@@ -179,7 +179,7 @@ protected:
+   // Static hash functions.  They don't depend on the context
+   // (ExprManager and such), so it is still thread-safe to have them
+   // static.
+-  static std::hash<char*> s_charHash;
++  static std::hash<const char*> s_charHash;
+   static std::hash<long int> s_intHash;
+ 
+   static size_t pointerHash(void* p) { return s_intHash((long int)p); }
+diff --git a/src/theory_core/theory_core.cpp b/src/theory_core/theory_core.cpp
+index df5289f..37ccab9 100644
+--- a/src/theory_core/theory_core.cpp
++++ b/src/theory_core/theory_core.cpp
+@@ -710,7 +710,7 @@ TheoryCore::TheoryCore(ContextManager* cm,
+     //    d_termTheorems(cm->getCurrentContext()),
+     d_predicates(cm->getCurrentContext()),
+     d_solver(NULL),
+-    d_simplifyInPlace(false),
++    d_simplifyInPlace(NULL),
+     d_currentRecursiveSimplifier(NULL),
+     d_resourceLimit(0),
+     d_timeBase(0),
diff --git a/nixpkgs/pkgs/applications/science/logic/cvc3/default.nix b/nixpkgs/pkgs/applications/science/logic/cvc3/default.nix
new file mode 100644
index 000000000000..ff481fd7ab46
--- /dev/null
+++ b/nixpkgs/pkgs/applications/science/logic/cvc3/default.nix
@@ -0,0 +1,34 @@
+{ stdenv, fetchurl, flex, bison, gmp, perl }:
+
+stdenv.mkDerivation rec {
+    pname = "cvc3";
+    version = "2.4.1";
+
+    src = fetchurl {
+      url = "http://www.cs.nyu.edu/acsys/cvc3/releases/${version}/${pname}-${version}.tar.gz";
+      sha256 = "1xxcwhz3y6djrycw8sm6xz83wb4hb12rd1n0skvc7fng0rh1snym";
+    };
+
+  buildInputs = [ gmp flex bison perl ];
+
+  patches = [ ./cvc3-2.4.1-gccv6-fix.patch ];
+
+  preConfigure = ''
+    sed -e "s@ /bin/bash@bash@g" -i Makefile.std
+    find . -exec sed -e "s@/usr/bin/perl@${perl}/bin/perl@g" -i '{}' ';'
+  '';
+
+  meta = with stdenv.lib; {
+    description = "A prover for satisfiability modulo theory (SMT)";
+    maintainers = with maintainers;
+      [ raskin ];
+    platforms = platforms.linux;
+    license = licenses.free;
+    homepage = "http://www.cs.nyu.edu/acsys/cvc3/index.html";
+  };
+  passthru = {
+    updateInfo = {
+      downloadPage = "http://www.cs.nyu.edu/acsys/cvc3/download.html";
+    };
+  };
+}