Merge commit 'e4134747f5666bcab8680aff67fa3b63384f9a0f'

27 files changed, 83 insertions, 162 deletions

diff --git a/nixpkgs/pkgs/applications/science/logic/aiger/default.nix b/nixpkgs/pkgs/applications/science/logic/aiger/default.nix
index 10d94e2bb8c7..0f65c9b7eaea 100644
--- a/nixpkgs/pkgs/applications/science/logic/aiger/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/aiger/default.nix
@@ -50,6 +50,6 @@ stdenv.mkDerivation rec {
     homepage    = http://fmv.jku.at/aiger/;
     license     = stdenv.lib.licenses.mit;
     maintainers = with stdenv.lib.maintainers; [ thoughtpolice ];
-    platforms   = stdenv.lib.platforms.linux;
+    platforms   = stdenv.lib.platforms.unix;
   };
 }
diff --git a/nixpkgs/pkgs/applications/science/logic/aspino/default.nix b/nixpkgs/pkgs/applications/science/logic/aspino/default.nix
index d6190942efab..82458d7c5663 100644
--- a/nixpkgs/pkgs/applications/science/logic/aspino/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/aspino/default.nix
@@ -40,10 +40,10 @@ stdenv.mkDerivation {
 
   meta = with stdenv.lib; {
     description = "SAT/PseudoBoolean/MaxSat/ASP solver using glucose";
-    maintainers = with maintainers; [ gebner ma27 ];
+    maintainers = with maintainers; [ gebner ];
     platforms = platforms.unix;
     license = licenses.asl20;
-    homepage = http://alviano.net/software/maxino/;
+    homepage = https://alviano.net/software/maxino/;
     # See pkgs/applications/science/logic/glucose/default.nix
     badPlatforms = [ "aarch64-linux" ];
   };
diff --git a/nixpkgs/pkgs/applications/science/logic/avy/default.nix b/nixpkgs/pkgs/applications/science/logic/avy/default.nix
index 9b59828ddab7..b43e0c6fbf1a 100644
--- a/nixpkgs/pkgs/applications/science/logic/avy/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/avy/default.nix
@@ -12,14 +12,14 @@ stdenv.mkDerivation {
   };
 
   buildInputs = [ cmake zlib boost.out boost.dev ];
-  NIX_CFLAGS_COMPILE = [ "-Wno-narrowing" ]
+  NIX_CFLAGS_COMPILE = toString ([ "-Wno-narrowing" ]
     # Squelch endless stream of warnings on same few things
     ++ stdenv.lib.optionals stdenv.cc.isClang [
       "-Wno-empty-body"
       "-Wno-tautological-compare"
       "-Wc++11-compat-deprecated-writable-strings"
       "-Wno-deprecated"
-    ];
+    ]);
 
   prePatch = ''
     sed -i -e '1i#include <stdint.h>' abc/src/bdd/dsd/dsd.h
diff --git a/nixpkgs/pkgs/applications/science/logic/boolector/default.nix b/nixpkgs/pkgs/applications/science/logic/boolector/default.nix
index f1f74bcb5810..4cf0b0f1ea1e 100644
--- a/nixpkgs/pkgs/applications/science/logic/boolector/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/boolector/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchFromGitHub
+{ stdenv, fetchFromGitHub, fetchpatch
 , cmake, lingeling, btor2tools
 }:
 
@@ -13,6 +13,14 @@ stdenv.mkDerivation rec {
     sha256 = "15i3ni5klss423m57wcy1gx0m5wfrjmglapwg85pm7fb3jj1y7sz";
   };
 
+  patches = [
+    (fetchpatch {
+      name = "CVE-2019-7560.patch";
+      url = "https://github.com/Boolector/boolector/commit/8d979d02e0482c7137c9f3a34e6d430dbfd1f5c5.patch";
+      sha256 = "1a1g02mk8b0azzjcigdn5zpshn0dn05fciwi8sd5q38yxvnvpbbi";
+    })
+  ];
+
   nativeBuildInputs = [ cmake ];
   buildInputs = [ lingeling btor2tools ];
 
diff --git a/nixpkgs/pkgs/applications/science/logic/btor2tools/default.nix b/nixpkgs/pkgs/applications/science/logic/btor2tools/default.nix
index 2d00e9f30464..2aedfb1d07ec 100644
--- a/nixpkgs/pkgs/applications/science/logic/btor2tools/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/btor2tools/default.nix
@@ -24,8 +24,8 @@ stdenv.mkDerivation {
   outputs = [ "out" "dev" "lib" ];
 
   meta = with stdenv.lib; {
-    description = "Fast SAT solver";
-    homepage    = http://fmv.jku.at/lingeling/;
+    description = "A generic parser and tool package for the BTOR2 format";
+    homepage    = "https://github.com/Boolector/btor2tools";
     license     = licenses.mit;
     platforms   = platforms.linux;
     maintainers = with maintainers; [ thoughtpolice ];
diff --git a/nixpkgs/pkgs/applications/science/logic/coq/default.nix b/nixpkgs/pkgs/applications/science/logic/coq/default.nix
index 99e9d856a717..ac001540e097 100644
--- a/nixpkgs/pkgs/applications/science/logic/coq/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/coq/default.nix
@@ -9,6 +9,7 @@
 , ocamlPackages, ncurses
 , buildIde ? true
 , glib, gnome3, wrapGAppsHook
+, darwin
 , csdp ? null
 , version
 }:
@@ -28,7 +29,10 @@ let
    "8.8.2" = "1lip3xja924dm6qblisk1bk0x8ai24s5xxqxphbdxj6djglj68fd";
    "8.9.0" = "1dkgdjc4n1m15m1p724hhi5cyxpqbjw6rxc5na6fl3v4qjjfnizh";
    "8.9.1" = "1xrq6mkhpq994bncmnijf8jwmwn961kkpl4mwwlv7j3dgnysrcv2";
-   "8.10+beta3" = "08c7q97jyblsf7dhk8jf1fx1cp9qr3dr5s42wigx10wh7i6j7pca";
+   "8.10.0" = "138jw94wp4mg5dgjc2asn8ng09ayz1mxdznq342n0m469j803gzg";
+   "8.10.1" = "072v2zkjzf7gj48137wpr3c9j0hg9pdhlr5l8jrgrwynld8fp7i4";
+   "8.10.2" = "0znxmpy71bfw0p6x47i82jf5k7v41zbz9bdpn901ysn3ir8l3wrz";
+   "8.11+beta1" = "06dlxj6v7gd51dh6ir121z7lgqdagkq717xxxrc8bdqhz7d2z7qj";
   }.${version};
   coq-version = stdenv.lib.versions.majorMinor version;
   versionAtLeast = stdenv.lib.versionAtLeast coq-version;
@@ -101,10 +105,13 @@ self = stdenv.mkDerivation {
   };
 
   nativeBuildInputs = [ pkgconfig ];
-  buildInputs = [ ncurses ] ++ (with ocamlPackages; [ ocaml findlib camlp5 num ])
+  buildInputs = [ ncurses ocamlPackages.ocaml ocamlPackages.findlib ]
+  ++ stdenv.lib.optional (!versionAtLeast "8.10") ocamlPackages.camlp5
+  ++ [ ocamlPackages.num ]
   ++ stdenv.lib.optionals buildIde
     (if versionAtLeast "8.10"
      then [ ocamlPackages.lablgtk3-sourceview3 glib gnome3.defaultIconTheme wrapGAppsHook ]
+     ++ stdenv.lib.optional stdenv.isDarwin darwin.apple_sdk.frameworks.Cocoa
      else [ ocamlPackages.lablgtk ]);
 
   postPatch = ''
@@ -119,7 +126,7 @@ self = stdenv.mkDerivation {
   setupHook = writeText "setupHook.sh" ''
     addCoqPath () {
       if test -d "''$1/lib/coq/${coq-version}/user-contrib"; then
-        export COQPATH="''${COQPATH}''${COQPATH:+:}''$1/lib/coq/${coq-version}/user-contrib/"
+        export COQPATH="''${COQPATH-}''${COQPATH:+:}''$1/lib/coq/${coq-version}/user-contrib/"
       fi
     }
 
@@ -136,7 +143,7 @@ self = stdenv.mkDerivation {
 
   prefixKey = "-prefix ";
 
-  buildFlags = "revision coq coqide bin/votour";
+  buildFlags = [ "revision" "coq" "coqide" "bin/votour" ];
 
   createFindlibDestdir = true;
 
diff --git a/nixpkgs/pkgs/applications/science/logic/elan/default.nix b/nixpkgs/pkgs/applications/science/logic/elan/default.nix
index f9a911d82108..e9ef16b2392b 100644
--- a/nixpkgs/pkgs/applications/science/logic/elan/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/elan/default.nix
@@ -4,7 +4,7 @@ rustPlatform.buildRustPackage rec {
   pname = "elan";
   version = "0.7.5";
 
-  cargoSha256 = "0lc320m3vw76d6pa5wp6c9jblac6lmyf9qqnxmsnkn4ixdhnghsd";
+  cargoSha256 = "0q0xlvyyf88dbz43r7kk9v8rrp6hj0nl5i2i9mg6ibk2gphgdv6v";
 
   src = fetchFromGitHub {
     owner = "kha";
diff --git a/nixpkgs/pkgs/applications/science/logic/eprover/default.nix b/nixpkgs/pkgs/applications/science/logic/eprover/default.nix
index 1f6fced22335..1b021f716078 100644
--- a/nixpkgs/pkgs/applications/science/logic/eprover/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/eprover/default.nix
@@ -2,11 +2,11 @@
 
 stdenv.mkDerivation rec {
   pname = "eprover";
-  version = "2.3";
+  version = "2.4";
 
   src = fetchurl {
     url = "https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_${version}/E.tgz";
-    sha256 = "15pbmi195812a2pwrvfa4gwad0cy7117d5kaw98651g6fzgd4rjk";
+    sha256 = "1xn5yypy6w36amsb3kvj1srlbv6v5dl51k64cd264asz2n469dxw";
   };
 
   buildInputs = [ which ];
diff --git a/nixpkgs/pkgs/applications/science/logic/hol_light/default.nix b/nixpkgs/pkgs/applications/science/logic/hol_light/default.nix
index 40b0115dc1b7..d799b52d115e 100644
--- a/nixpkgs/pkgs/applications/science/logic/hol_light/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/hol_light/default.nix
@@ -21,13 +21,13 @@ let
 in
 
 stdenv.mkDerivation {
-  name     = "hol_light-2019-03-27";
+  name     = "hol_light-2019-10-06";
 
   src = fetchFromGitHub {
     owner  = "jrh13";
     repo   = "hol-light";
-    rev    = "a2b487b38d9da47350f1b4316e34a8fa4cf7a40a";
-    sha256 = "1qlidl15qi8w4si8wxcmj8yg2srsb0q4k1ad9yd91sgx9h9aq8fk";
+    rev    = "5c91b2ded8a66db571824ecfc18b4536c103b23e";
+    sha256 = "0sxsk8z08ba0q5aixdyczcx5l29lb51ba4ip3d2fry7y604kjsx6";
   };
 
   buildInputs = [ ocaml camlp5 ];
@@ -45,6 +45,6 @@ stdenv.mkDerivation {
     homepage    = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
     license     = licenses.bsd2;
     platforms   = platforms.unix;
-    maintainers = with maintainers; [ thoughtpolice z77z vbgl ];
+    maintainers = with maintainers; [ thoughtpolice maggesi vbgl ];
   };
 }
diff --git a/nixpkgs/pkgs/applications/science/logic/jonprl/default.nix b/nixpkgs/pkgs/applications/science/logic/jonprl/default.nix
index 61ca78d85ed1..e503836098f1 100644
--- a/nixpkgs/pkgs/applications/science/logic/jonprl/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/jonprl/default.nix
@@ -30,5 +30,6 @@ stdenv.mkDerivation rec {
     license = stdenv.lib.licenses.mit;
     maintainers = with stdenv.lib.maintainers; [ puffnfresh ];
     platforms = stdenv.lib.platforms.linux;
+    broken = true;
   };
 }
diff --git a/nixpkgs/pkgs/applications/science/logic/lean2/default.nix b/nixpkgs/pkgs/applications/science/logic/lean2/default.nix
index 8cc50bb5e295..612c9d6f92a2 100644
--- a/nixpkgs/pkgs/applications/science/logic/lean2/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/lean2/default.nix
@@ -32,5 +32,6 @@ stdenv.mkDerivation {
     license     = licenses.asl20;
     platforms   = platforms.unix;
     maintainers = with maintainers; [ thoughtpolice gebner ];
+    broken = true;
   };
 }
diff --git a/nixpkgs/pkgs/applications/science/logic/lingeling/default.nix b/nixpkgs/pkgs/applications/science/logic/lingeling/default.nix
index 287dbd36eabf..94be89d4736f 100644
--- a/nixpkgs/pkgs/applications/science/logic/lingeling/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/lingeling/default.nix
@@ -43,7 +43,7 @@ stdenv.mkDerivation {
     description = "Fast SAT solver";
     homepage    = http://fmv.jku.at/lingeling/;
     license     = licenses.mit;
-    platforms   = platforms.linux;
+    platforms   = platforms.unix;
     maintainers = with maintainers; [ thoughtpolice ];
   };
 }
diff --git a/nixpkgs/pkgs/applications/science/logic/mcrl2/default.nix b/nixpkgs/pkgs/applications/science/logic/mcrl2/default.nix
index 93212c5b8546..a479e31e3395 100644
--- a/nixpkgs/pkgs/applications/science/logic/mcrl2/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/mcrl2/default.nix
@@ -1,4 +1,4 @@
-{stdenv, fetchurl, cmake, libGLU_combined, qt5, boost}:
+{stdenv, fetchurl, cmake, libGLU, libGL, qt5, boost}:
 
 stdenv.mkDerivation rec {
   version = "201707";
@@ -10,7 +10,7 @@ stdenv.mkDerivation rec {
     sha256 = "1c8h94ja7271ph61zrcgnjgblxppld6v22f7f900prjgzbcfy14m";
   };
 
-  buildInputs = [ cmake libGLU_combined qt5.qtbase boost ];
+  buildInputs = [ cmake libGLU libGL qt5.qtbase boost ];
 
   enableParallelBuilding = true;
 
diff --git a/nixpkgs/pkgs/applications/science/logic/minisat/clang.diff b/nixpkgs/pkgs/applications/science/logic/minisat/clang.diff
deleted file mode 100644
index 5b5072c71f3f..000000000000
--- a/nixpkgs/pkgs/applications/science/logic/minisat/clang.diff
+++ /dev/null
@@ -1,45 +0,0 @@
-diff -aur minisat/core/SolverTypes.h minisat.clang/core/SolverTypes.h
---- minisat/core/SolverTypes.h	2010-07-10 18:07:36.000000000 +0200
-+++ minisat.clang/core/SolverTypes.h	2016-05-13 12:14:50.759671959 +0200
-@@ -47,7 +47,7 @@
-     int     x;
- 
-     // Use this as a constructor:
--    friend Lit mkLit(Var var, bool sign = false);
-+    //friend Lit mkLit(Var var, bool sign = false);
- 
-     bool operator == (Lit p) const { return x == p.x; }
-     bool operator != (Lit p) const { return x != p.x; }
-@@ -55,7 +55,7 @@
- };
- 
- 
--inline  Lit  mkLit     (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
-+inline  Lit  mkLit     (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }
- inline  Lit  operator ~(Lit p)              { Lit q; q.x = p.x ^ 1; return q; }
- inline  Lit  operator ^(Lit p, bool b)      { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
- inline  bool sign      (Lit p)              { return p.x & 1; }
-diff -aur minisat/utils/Options.h minisat.clang/utils/Options.h
---- minisat/utils/Options.h	2010-07-10 18:07:36.000000000 +0200
-+++ minisat.clang/utils/Options.h	2016-05-13 12:14:50.759671959 +0200
-@@ -282,15 +282,15 @@
-         if (range.begin == INT64_MIN)
-             fprintf(stderr, "imin");
-         else
--            fprintf(stderr, "%4"PRIi64, range.begin);
-+            fprintf(stderr, "%4" PRIi64, range.begin);
- 
-         fprintf(stderr, " .. ");
-         if (range.end == INT64_MAX)
-             fprintf(stderr, "imax");
-         else
--            fprintf(stderr, "%4"PRIi64, range.end);
-+            fprintf(stderr, "%4" PRIi64, range.end);
- 
--        fprintf(stderr, "] (default: %"PRIi64")\n", value);
-+        fprintf(stderr, "] (default: %" PRIi64 ")\n", value);
-         if (verbose){
-             fprintf(stderr, "\n        %s\n", description);
-             fprintf(stderr, "\n");
-Only in minisat.clang/utils: Options.o
-Only in minisat.clang/utils: System.o
diff --git a/nixpkgs/pkgs/applications/science/logic/minisat/darwin.patch b/nixpkgs/pkgs/applications/science/logic/minisat/darwin.patch
deleted file mode 100644
index f2b618d6bb3a..000000000000
--- a/nixpkgs/pkgs/applications/science/logic/minisat/darwin.patch
+++ /dev/null
@@ -1,26 +0,0 @@
-https://github.com/fasterthanlime/homebrew-mingw/blob/master/Library/Formula/minisat.rb
-
-diff --git a/utils/System.cc b/utils/System.cc
-index a7cf53f..feeaf3c 100644
---- a/utils/System.cc
-+++ b/utils/System.cc
-@@ -78,16 +78,17 @@ double Minisat::memUsed(void) {
-     struct rusage ru;
-     getrusage(RUSAGE_SELF, &ru);
-     return (double)ru.ru_maxrss / 1024; }
--double MiniSat::memUsedPeak(void) { return memUsed(); }
-+double Minisat::memUsedPeak(void) { return memUsed(); }
- 
- 
- #elif defined(__APPLE__)
- #include <malloc/malloc.h>
- 
--double Minisat::memUsed(void) {
-+double Minisat::memUsed() {
-     malloc_statistics_t t;
-     malloc_zone_statistics(NULL, &t);
-     return (double)t.max_size_in_use / (1024*1024); }
-+double Minisat::memUsedPeak() { return memUsed(); }
- 
- #else
- double Minisat::memUsed() { 
diff --git a/nixpkgs/pkgs/applications/science/logic/minisat/default.nix b/nixpkgs/pkgs/applications/science/logic/minisat/default.nix
index 34051a1da404..6b642832b83f 100644
--- a/nixpkgs/pkgs/applications/science/logic/minisat/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/minisat/default.nix
@@ -1,27 +1,19 @@
-{ stdenv, fetchurl, zlib }:
+{ stdenv, fetchFromGitHub, cmake, zlib }:
 
 stdenv.mkDerivation rec {
   pname = "minisat";
-  version = "2.2.0";
+  version = "2.2.1";
 
-  src = fetchurl {
-    url = "http://minisat.se/downloads/${pname}-${version}.tar.gz";
-    sha256 = "023qdnsb6i18yrrawlhckm47q8x0sl7chpvvw3gssfyw3j2pv5cj";
+  src = fetchFromGitHub {
+    owner = "stp";
+    repo = pname;
+    rev = "releases/${version}";
+    sha256 = "14vcbjnlia00lpyv2fhbmw3wbc9bk9h7bln9zpyc3nwiz5cbjz4a";
   };
 
-  patches =
-    [ ./darwin.patch ]
-    ++ stdenv.lib.optionals stdenv.cc.isClang [ ./clang.diff ];
-
+  nativeBuildInputs = [ cmake ];
   buildInputs = [ zlib ];
 
-  preBuild = "cd simp";
-  makeFlags = [ "r" "MROOT=.." ];
-  installPhase = ''
-    mkdir -p $out/bin
-    cp minisat_release $out/bin/minisat
-  '';
-
   meta = with stdenv.lib; {
     description = "Compact and readable SAT solver";
     maintainers = with maintainers; [ gebner raskin ];
diff --git a/nixpkgs/pkgs/applications/science/logic/minisat/unstable.nix b/nixpkgs/pkgs/applications/science/logic/minisat/unstable.nix
deleted file mode 100644
index ef46c694acb7..000000000000
--- a/nixpkgs/pkgs/applications/science/logic/minisat/unstable.nix
+++ /dev/null
@@ -1,23 +0,0 @@
-{ stdenv, fetchFromGitHub, zlib, cmake }:
-
-stdenv.mkDerivation {
-  name = "minisat-unstable-2013-09-25";
-
-  src = fetchFromGitHub {
-    owner = "niklasso";
-    repo = "minisat";
-    rev = "37dc6c67e2af26379d88ce349eb9c4c6160e8543";
-    sha256 = "091hf3qkm197s5r7xcr3m07xsdwyz2rqk1hc9kj0hn13imz09irq";
-  };
-
-  buildInputs = [ zlib ];
-  nativeBuildInputs =  [ cmake ];
-
-  meta = with stdenv.lib; {
-    description = "Compact and readable SAT solver";
-    maintainers = with maintainers; [ mic92 ];
-    platforms = platforms.unix;
-    license = licenses.mit;
-    homepage = http://minisat.se/;
-  };
-}
diff --git a/nixpkgs/pkgs/applications/science/logic/monosat/default.nix b/nixpkgs/pkgs/applications/science/logic/monosat/default.nix
index 30d47687a3eb..c0512b744884 100644
--- a/nixpkgs/pkgs/applications/science/logic/monosat/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/monosat/default.nix
@@ -8,11 +8,11 @@ with stdenv.lib;
 let
   boolToCmake = x: if x then "ON" else "OFF";
 
-  rev    = "2deeadeff214e975c9f7508bc8a24fa05a1a0c32";
-  sha256 = "09yhym2lxmn3xbhw5fcxawnmvms5jd9fw9m7x2wzil7yvy4vwdjn";
+  rev    = "1.8.0";
+  sha256 = "0q3a8x3iih25xkp2bm842sm2hxlb8hxlls4qmvj7vzwrh4lvsl7b";
 
   pname   = "monosat";
-  version = substring 0 7 sha256;
+  version = rev;
 
   src = fetchFromGitHub {
     owner = "sambayless";
@@ -25,7 +25,11 @@ let
     inherit src;
     buildInputs = [ cmake zlib gmp jdk8 ];
 
-    cmakeFlags = [ "-DJAVA=${boolToCmake includeJava}" "-DGPL=${boolToCmake includeGplCode}" ];
+    cmakeFlags = [
+      "-DBUILD_STATIC=OFF"
+      "-DJAVA=${boolToCmake includeJava}"
+      "-DGPL=${boolToCmake includeGplCode}"
+    ];
 
     postInstall = optionalString includeJava ''
       mkdir -p $out/share/java
@@ -39,6 +43,7 @@ let
       platforms   = platforms.unix;
       license     = if includeGplCode then licenses.gpl2 else licenses.mit;
       homepage    = https://github.com/sambayless/monosat;
+      maintainers = [ maintainers.acairncross ];
     };
   };
 
@@ -50,18 +55,15 @@ let
 
     propagatedBuildInputs = [ core cython ];
 
-    # This tells setup.py to use cython
+    # This tells setup.py to use cython, which should produce faster bindings
     MONOSAT_CYTHON = true;
 
     # The relative paths here don't make sense for our Nix build
-    # Also, let's use cython since it should produce faster bindings
     # TODO: do we want to just reference the core monosat library rather than copying the
     # shared lib? The current setup.py copies the .dylib/.so...
     postPatch = ''
-
       substituteInPlace setup.py \
-        --replace '../../../../libmonosat.dylib' '${core}/lib/libmonosat.dylib' \
-        --replace '../../../../libmonosat.so'  '${core}/lib/libmonosat.so'
+        --replace 'library_dir = "../../../../"' 'library_dir = "${core}/lib/"'
     '';
   };
-in core
\ No newline at end of file
+in core
diff --git a/nixpkgs/pkgs/applications/science/logic/ott/default.nix b/nixpkgs/pkgs/applications/science/logic/ott/default.nix
index 40c66dd699d8..854a62a5538d 100644
--- a/nixpkgs/pkgs/applications/science/logic/ott/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/ott/default.nix
@@ -2,13 +2,13 @@
 
 stdenv.mkDerivation rec {
   pname = "ott";
-  version = "0.28";
+  version = "0.29";
 
   src = fetchFromGitHub {
     owner = "ott-lang";
     repo = "ott";
     rev = version;
-    sha256 = "0mzbrvqayqpns9zzg4m1scxx24dv9askhn51dawyb9pisvlyvai0";
+    sha256 = "0saznk2mjbhp3j57imy2p2j0938026bw5m5gqbj59vcvk1rwwl22";
   };
 
   nativeBuildInputs = [ pkgconfig ];
diff --git a/nixpkgs/pkgs/applications/science/logic/potassco/clingo.nix b/nixpkgs/pkgs/applications/science/logic/potassco/clingo.nix
index 2b368a0e6730..7c1ee8099e2c 100644
--- a/nixpkgs/pkgs/applications/science/logic/potassco/clingo.nix
+++ b/nixpkgs/pkgs/applications/science/logic/potassco/clingo.nix
@@ -2,15 +2,14 @@
 
 stdenv.mkDerivation rec {
   pname = "clingo";
-  version = "5.3.0";
+  version = "5.4.0";
 
   src = fetchzip {
     url = "https://github.com/potassco/clingo/archive/v${version}.tar.gz";
-    sha256 = "01czx26p8gv81ahrh650x208hjhd8bx1kb688fmk1m4pw4yg5bfv";
+    sha256 = "0gfqlgwg3qx042w6hdc9qpmr50n4vci3p0ddk28f3kqacf6q9q7m";
   };
 
-  buildInputs = [];
-  nativeBuildInputs = [cmake];
+  nativeBuildInputs = [ cmake ];
 
   cmakeFlags = [ "-DCLINGO_BUILD_WITH_PYTHON=OFF" ];
 
diff --git a/nixpkgs/pkgs/applications/science/logic/prover9/default.nix b/nixpkgs/pkgs/applications/science/logic/prover9/default.nix
index a4538e1070a3..9528a5942a43 100644
--- a/nixpkgs/pkgs/applications/science/logic/prover9/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/prover9/default.nix
@@ -21,7 +21,7 @@ stdenv.mkDerivation {
     done
   '';
 
-  buildFlags = "all";
+  buildFlags = [ "all" ];
 
   checkPhase = "make test1";
 
diff --git a/nixpkgs/pkgs/applications/science/logic/stp/default.nix b/nixpkgs/pkgs/applications/science/logic/stp/default.nix
index 0ea659d1927f..dd00eda1b571 100644
--- a/nixpkgs/pkgs/applications/science/logic/stp/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/stp/default.nix
@@ -1,4 +1,5 @@
-{ stdenv, cmake, boost, bison, flex, fetchFromGitHub, perl, python3, python3Packages, zlib, minisatUnstable, cryptominisat }:
+{ stdenv, cmake, boost, bison, flex, fetchFromGitHub, perl
+, python3, python3Packages, zlib, minisat, cryptominisat }:
 
 stdenv.mkDerivation rec {
   pname = "stp";
@@ -11,7 +12,7 @@ stdenv.mkDerivation rec {
     sha256 = "1yg2v4wmswh1sigk47drwsxyayr472mf4i47lqmlcgn9hhbx1q87";
   };
 
-  buildInputs = [ boost zlib minisatUnstable cryptominisat python3 ];
+  buildInputs = [ boost zlib minisat cryptominisat python3 ];
   nativeBuildInputs = [ cmake bison flex perl ];
   preConfigure = ''
     python_install_dir=$out/${python3Packages.python.sitePackages}
diff --git a/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix b/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix
index ed66c77dcabf..ddefcf1b3aa2 100644
--- a/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix
@@ -1,18 +1,20 @@
-{ stdenv, fetchFromGitHub, yosys, bash, python3 }:
+{ stdenv, fetchFromGitHub, yosys, bash, python3, yices }:
 
 stdenv.mkDerivation {
   pname = "symbiyosys";
-  version = "2019.08.13";
+  version = "2019.10.11";
 
   src = fetchFromGitHub {
     owner  = "yosyshq";
     repo   = "symbiyosys";
-    rev    = "9cb542ac7a310b3dfa626349db53bed6236b670c";
-    sha256 = "0c7nz740738ybk33zzlfl00cq86n31wvra8pqqkpl4ygxnwca1d6";
+    rev    = "23f89011b678daa9da406d4f45f790e45f8f68ca";
+    sha256 = "01596yvfj79iywwczjwlb2l9qnh7bsj7jff66jdk1ybjnxf841f0";
   };
 
   buildInputs = [ python3 yosys ];
 
+  propagatedBuildInputs = [ yices ];
+
   buildPhase = "true";
   installPhase = ''
     mkdir -p $out/bin $out/share/yosys/python3
diff --git a/nixpkgs/pkgs/applications/science/logic/tamarin-prover/default.nix b/nixpkgs/pkgs/applications/science/logic/tamarin-prover/default.nix
index 40378f8c04d5..9b87b8c899e5 100644
--- a/nixpkgs/pkgs/applications/science/logic/tamarin-prover/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/tamarin-prover/default.nix
@@ -104,4 +104,6 @@ mkDerivation (common "tamarin-prover" src // {
           tamarin-prover-term
           tamarin-prover-theory
         ];
+
+  broken = true;
 })
diff --git a/nixpkgs/pkgs/applications/science/logic/why3/default.nix b/nixpkgs/pkgs/applications/science/logic/why3/default.nix
index 6f338f214783..eeb3a6b6d361 100644
--- a/nixpkgs/pkgs/applications/science/logic/why3/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/why3/default.nix
@@ -3,11 +3,11 @@
 
 stdenv.mkDerivation {
   pname = "why3";
-  version = "1.2.0";
+  version = "1.2.1";
 
   src = fetchurl {
-    url = https://gforge.inria.fr/frs/download.php/file/37903/why3-1.2.0.tar.gz;
-    sha256 = "0xz001jhi71ja8vqrjz27v63bidrzj4qvg1yqarq6p4dmpxhk348";
+    url = https://gforge.inria.fr/frs/download.php/file/38185/why3-1.2.1.tar.gz;
+    sha256 = "014gkwisjp05x3342zxkryb729p02ngx1hcjjsrplpa53jzgz647";
   };
 
   buildInputs = with ocamlPackages; [
diff --git a/nixpkgs/pkgs/applications/science/logic/yices/default.nix b/nixpkgs/pkgs/applications/science/logic/yices/default.nix
index 76ed934fb39e..b8dd528a11c1 100644
--- a/nixpkgs/pkgs/applications/science/logic/yices/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/yices/default.nix
@@ -28,7 +28,7 @@ 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 = let
-    ver_XdotY = builtins.concatStringsSep "." (stdenv.lib.take 2 (stdenv.lib.splitString "." version));
+    ver_XdotY = stdenv.lib.versions.majorMinor version;
   in ''
       make install LDCONFIG=true
       ln -sfr $out/lib/libyices.so.{${version},${ver_XdotY}}
diff --git a/nixpkgs/pkgs/applications/science/logic/z3/default.nix b/nixpkgs/pkgs/applications/science/logic/z3/default.nix
index 14f75fb68b5e..170a56b95b91 100644
--- a/nixpkgs/pkgs/applications/science/logic/z3/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/z3/default.nix
@@ -2,13 +2,13 @@
 
 stdenv.mkDerivation rec {
   pname = "z3";
-  version = "4.8.5";
+  version = "4.8.7";
 
   src = fetchFromGitHub {
     owner  = "Z3Prover";
     repo   = pname;
-    rev    = "Z3-${version}";
-    sha256 = "11sy98clv7ln0a5vqxzvh6wwqbswsjbik2084hav5kfws4xvklfa";
+    rev    = "z3-${version}";
+    sha256 = "0hprcdwhhyjigmhhk6514m71bnmvqci9r8gglrqilgx424r6ff7q";
   };
 
   buildInputs = [ python fixDarwinDylibNames ];