5 files changed, 43 insertions, 25 deletions
diff --git a/pkgs/applications/science/logic/abc/default.nix b/pkgs/applications/science/logic/abc/default.nix
index bab9b302d7d1..6e7a3cfc88ac 100644
--- a/pkgs/applications/science/logic/abc/default.nix
+++ b/pkgs/applications/science/logic/abc/default.nix
@@ -1,20 +1,21 @@
-{ fetchhg, stdenv, readline }:
+{ fetchFromGitHub, stdenv, readline, cmake }:
 
 stdenv.mkDerivation rec {
   name = "abc-verifier-${version}";
-  version = "20160818";
+  version = "2018-07-08";
 
-  src = fetchhg {
-    url    = "https://bitbucket.org/alanmi/abc";
-    rev    = "a2e5bc66a68a72ccd267949e5c9973dd18f8932a";
-    sha256 = "09yvhj53af91nc54gmy7cbp7yljfcyj68a87494r5xvdfnsj11gy";
+  src = fetchFromGitHub {
+    owner = "berkeley-abc";
+    repo = "abc";
+    rev    = "24407e13db4b8ca16c3996049b2d33ec3722de39";
+    sha256 = "1rckji7nk81n6v1yajz7daqwipxacv7zlafknvmbiwji30j47sq5";
   };
 
+  nativeBuildInputs = [ cmake ];
   buildInputs = [ readline ];
-  preBuild = ''
-    export buildFlags="CC=$CC CXX=$CXX LD=$CXX"
-  '';
+
   enableParallelBuilding = true;
+
   installPhase = ''
     mkdir -p $out/bin
     mv abc $out/bin
@@ -22,7 +23,7 @@ stdenv.mkDerivation rec {
 
   meta = {
     description = "A tool for squential logic synthesis and formal verification";
-    homepage    = "https://people.eecs.berkeley.edu/~alanmi/abc/abc.htm";
+    homepage    = https://people.eecs.berkeley.edu/~alanmi/abc;
     license     = stdenv.lib.licenses.mit;
     platforms   = stdenv.lib.platforms.unix;
     maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
diff --git a/pkgs/applications/science/logic/cvc4/default.nix b/pkgs/applications/science/logic/cvc4/default.nix
index 222021bb1c9f..cddcbef7a035 100644
--- a/pkgs/applications/science/logic/cvc4/default.nix
+++ b/pkgs/applications/science/logic/cvc4/default.nix
@@ -35,7 +35,7 @@ stdenv.mkDerivation rec {
 
   meta = with stdenv.lib; {
     description = "A high-performance theorem prover and SMT solver";
-    homepage    = http://cvc4.cs.nyu.edu/web/;
+    homepage    = http://cvc4.cs.stanford.edu/web/;
     license     = licenses.gpl3;
     platforms   = platforms.unix;
     maintainers = with maintainers; [ vbgl thoughtpolice gebner ];
diff --git a/pkgs/applications/science/logic/poly/default.nix b/pkgs/applications/science/logic/poly/default.nix
index 1b401c927b6e..2f765572f9ad 100644
--- a/pkgs/applications/science/logic/poly/default.nix
+++ b/pkgs/applications/science/logic/poly/default.nix
@@ -1,17 +1,20 @@
-{stdenv, fetchurl, gmp, cmake, python}:
+{stdenv, fetchFromGitHub, gmp, cmake, python}:
 
-let version = "0.1.4";
-in
+stdenv.mkDerivation rec {
+  name = "${pname}-${version}";
+  pname = "libpoly";
+  version = "0.1.7";
 
-stdenv.mkDerivation {
-  name = "libpoly-${version}";
-
-  src = fetchurl {
-    url = "https://github.com/SRI-CSL/libpoly/archive/v${version}.tar.gz";
-    sha256 = "16x1pk2a3pcb5a0dzyw28ccjwkhmbsck4hy80ss7kx0dd7qgpi7j";
+  src = fetchFromGitHub {
+    owner = "SRI-CSL";
+    repo = "libpoly";
+    rev = "v${version}";
+    sha256 = "0i5ar4lhs88glk0rvkmag656ii434i6i1q5dspx6d0kyg78fii64";
   };
 
-  buildInputs = [ cmake gmp python ];
+  nativeBuildInputs = [ cmake ];
+
+  buildInputs = [ gmp python ];
 
   meta = with stdenv.lib; {
     homepage = https://github.com/SRI-CSL/libpoly;
diff --git a/pkgs/applications/science/logic/yices/default.nix b/pkgs/applications/science/logic/yices/default.nix
index a607f1066395..3121a83e5b98 100644
--- a/pkgs/applications/science/logic/yices/default.nix
+++ b/pkgs/applications/science/logic/yices/default.nix
@@ -2,12 +2,12 @@
 
 stdenv.mkDerivation rec {
   name    = "yices-${version}";
-  version = "2.5.4";
+  version = "2.6.0";
 
   src = fetchurl {
     url = "https://github.com/SRI-CSL/yices2/archive/Yices-${version}.tar.gz";
     name = "${name}-src.tar.gz";
-    sha256 = "1k8wmlddi3zv5kgg6xbch3a0s0xqsmsfc7y6z8zrgcyhswl36h7p";
+    sha256 = "10ikq7ib8jhx7hlxfm6mp5qg6r8dflqs8242q5zaicn80qixpm12";
   };
 
   nativeBuildInputs = [ autoreconfHook ];
@@ -26,9 +26,11 @@ stdenv.mkDerivation rec {
 
   # Includes a fix for the embedded soname being libyices.so.2.5, but
   # only installing the libyices.so.2.5.x file.
-  installPhase = ''
+  installPhase = let
+    ver_XdotY = builtins.concatStringsSep "." (stdenv.lib.take 2 (stdenv.lib.splitString "." version));
+  in ''
       make install LDCONFIG=true
-      (cd $out/lib && ln -s -f libyices.so.${version} libyices.so.2.5)
+      ln -sfr $out/lib/libyices.so.{${version},${ver_XdotY}}
   '';
 
   meta = with stdenv.lib; {
diff --git a/pkgs/applications/science/logic/z3/default.nix b/pkgs/applications/science/logic/z3/default.nix
index 54c9799a01b8..1cbe914779e6 100644
--- a/pkgs/applications/science/logic/z3/default.nix
+++ b/pkgs/applications/science/logic/z3/default.nix
@@ -20,6 +20,18 @@ stdenv.mkDerivation rec {
     cd build
   '';
 
+  postInstall = ''
+    mkdir -p $dev $lib $python/lib
+
+    mv $out/lib/python*  $python/lib/
+    mv $out/lib          $lib/lib
+    mv $out/include      $dev/include
+
+    ln -sf $lib/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary} $python/${python.sitePackages}/z3/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary}
+  '';
+
+  outputs = [ "out" "lib" "dev" "python" ];
+
   meta = {
     description = "A high-performance theorem prover and SMT solver";
     homepage    = "https://github.com/Z3Prover/z3";