diff --git a/pkgs/applications/science/logic/boolector/default.nix b/pkgs/applications/science/logic/boolector/default.nix
index aedc8e3484a9..0364a76639aa 100644
--- a/pkgs/applications/science/logic/boolector/default.nix
+++ b/pkgs/applications/science/logic/boolector/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchFromGitHub, lib, python3
+{ stdenv, fetchFromGitHub, fetchpatch, lib, python3
 , cmake, lingeling, btor2tools, gtest, gmp
 }:
 
@@ -13,6 +13,14 @@ stdenv.mkDerivation rec {
     sha256 = "0jkmaw678njqgkflzj9g374yk1mci8yqvsxkrqzlifn6bwhwb7ci";
   };
 
+  # excludes development artifacts from install, will be included in next release
+  patches = [
+    (fetchpatch {
+      url = "https://github.com/Boolector/boolector/commit/4d240436e34e65096671099766344dd9126145b1.patch";
+      sha256 = "1girsbvlhkkl1hldl2gsjynwc3m92jskn798qhx0ydg6whrfgcgw";
+    })
+  ];
+
   postPatch = ''
     sed s@REPLACEME@file://${gtest.src}@ ${./cmake-gtest.patch} | patch -p1
   '';
@@ -23,39 +31,39 @@ stdenv.mkDerivation rec {
   cmakeFlags =
     [ "-DBUILD_SHARED_LIBS=ON"
       "-DUSE_LINGELING=YES"
-      "-DBtor2Tools_INCLUDE_DIR=${btor2tools.dev}/include"
-      "-DBtor2Tools_LIBRARIES=${btor2tools.lib}/lib/libbtor2parser.so"
     ] ++ (lib.optional (gmp != null) "-DUSE_GMP=YES");
 
-  installPhase = ''
-    mkdir -p $out/bin $lib/lib $dev/include
-
-    cp -vr bin/* $out/bin
-    cp -vr lib/* $lib/lib
-
-    rm -rf $out/bin/{examples,tests}
-    # we don't care about gtest related libs
-    rm -rf $lib/lib/libg*
-
-    cd ../src
-    find . -iname '*.h' -exec cp --parents '{}' $dev/include \;
-    rm -rf $dev/include/tests
-  '';
-
   checkInputs = [ python3 ];
   doCheck = true;
-  preCheck = ''
-    export LD_LIBRARY_PATH=$(readlink -f lib)
-    patchShebangs ..
+  preCheck =
+    let var = if stdenv.isDarwin then "DYLD_LIBRARY_PATH" else "LD_LIBRARY_PATH";
+    in
+      # tests modelgen and modelgensmt2 spawn boolector in another processes and
+      # macOS strips DYLD_LIBRARY_PATH, hardcode it for testing
+      stdenv.lib.optionalString stdenv.isDarwin ''
+        cp -r bin bin.back
+        install_name_tool -change libboolector.dylib $(pwd)/lib/libboolector.dylib bin/boolector
+      '' + ''
+        export ${var}=$(readlink -f lib)
+        patchShebangs ..
+      '';
+
+  postCheck = stdenv.lib.optionalString stdenv.isDarwin ''
+    rm -rf bin
+    mv bin.back bin
   '';
 
-  outputs = [ "out" "dev" "lib" ];
+  # this is what haskellPackages.boolector expects
+  postInstall = ''
+    cp $out/include/boolector/boolector.h $out/include/boolector.h
+    cp $out/include/boolector/btortypes.h $out/include/btortypes.h
+  '';
 
   meta = with stdenv.lib; {
     description = "An extremely fast SMT solver for bit-vectors and arrays";
     homepage    = "https://boolector.github.io";
     license     = licenses.mit;
-    platforms   = platforms.linux;
+    platforms   = with platforms; linux ++ darwin;
     maintainers = with maintainers; [ thoughtpolice ];
   };
 }
diff --git a/pkgs/applications/science/logic/btor2tools/default.nix b/pkgs/applications/science/logic/btor2tools/default.nix
index 34c0dac2a17e..7d2aed7596e8 100644
--- a/pkgs/applications/science/logic/btor2tools/default.nix
+++ b/pkgs/applications/science/logic/btor2tools/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, cmake, fetchFromGitHub }:
+{ stdenv, cmake, fetchFromGitHub, fixDarwinDylibNames }:
 
 stdenv.mkDerivation rec {
   pname = "btor2tools";
@@ -11,7 +11,7 @@ stdenv.mkDerivation rec {
     sha256 = "0mfqmkgvyw8fa2c09kww107dmk180ch1hp98r5kv41vnc04iqb0s";
   };
 
-  nativeBuildInputs = [ cmake ];
+  nativeBuildInputs = [ cmake ] ++ stdenv.lib.optional stdenv.isDarwin fixDarwinDylibNames;
 
   installPhase = ''
     mkdir -p $out $dev/include/btor2parser/ $lib/lib