diff --git a/.ghci b/.ghci
deleted file mode 100644
--- a/.ghci
+++ /dev/null
@@ -1,1 +0,0 @@
-:set -isrc -idist/build/autogen -optP-include -optPdist/build/autogen/cabal_macros.h -optP-Iincludes
diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,7 @@
+0.4.6 [2019.05.20]
+------------------
+* Add support for `cryptominisat5`
+
 0.4.5 [2019.05.02]
 ------------------
 * Allow `ersatz-regexp-grid` to build with `base-4.13` (GHC 8.8).
diff --git a/ersatz.cabal b/ersatz.cabal
--- a/ersatz.cabal
+++ b/ersatz.cabal
@@ -1,5 +1,5 @@
 name:           ersatz
-version:        0.4.5
+version:        0.4.6
 license:        BSD3
 license-file:   LICENSE
 author:         Edward A. Kmett, Eric Mertens, Johan Kiviniemi
@@ -82,7 +82,6 @@
               , GHC == 8.6.5
               , GHC == 8.8.1
 extra-source-files:
-  .ghci
   .gitignore
   .hlint.yaml
   .travis.yml
diff --git a/examples/regexp-grid/Main.hs b/examples/regexp-grid/Main.hs
--- a/examples/regexp-grid/Main.hs
+++ b/examples/regexp-grid/Main.hs
@@ -11,7 +11,7 @@
 
 main :: IO ()
 main = do
-  (res, msol) <- solveWith cryptominisat problem
+  (res, msol) <- solveWith cryptominisat5 problem
   when (res /= Satisfied) (fail (show res))
   case msol of
     Nothing  -> fail "Sol was Nothing"
diff --git a/examples/sudoku/Main.hs b/examples/sudoku/Main.hs
--- a/examples/sudoku/Main.hs
+++ b/examples/sudoku/Main.hs
@@ -21,7 +21,7 @@
   putStr (render initValues)
 
   putStrLn "Solution:"
-  (res, msol) <- solveWith cryptominisat (problem initValues)
+  (res, msol) <- solveWith cryptominisat5 (problem initValues)
   when (res /= Satisfied) (fail (show res))
   case msol of
     Just sol -> putStr (render sol)
diff --git a/src/Ersatz/Solver/Minisat.hs b/src/Ersatz/Solver/Minisat.hs
--- a/src/Ersatz/Solver/Minisat.hs
+++ b/src/Ersatz/Solver/Minisat.hs
@@ -14,6 +14,8 @@
   ( minisat
   , cryptominisat
   , minisatPath
+  , cryptominisat5
+  , cryptominisat5Path
   ) where
 
 import Data.ByteString.Builder
@@ -68,3 +70,29 @@
                             in  if 0 == v then m else IntMap.insert (abs v) (v>0) m
                  ) IntMap.empty ys
     _ -> IntMap.empty -- WRONG (should be Nothing)
+
+-- | 'Solver' for 'SAT' problems that tries to invoke the @cryptominisat5@ executable from the @PATH@
+cryptominisat5 :: MonadIO m => Solver SAT m
+cryptominisat5 = cryptominisat5Path "cryptominisat5"
+
+-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes @cryptominisat5@ compatible arguments.
+--
+-- The 'FilePath' refers to the path to the executable.
+cryptominisat5Path :: MonadIO m => FilePath -> Solver SAT m
+cryptominisat5Path path problem = liftIO $
+  withTempFiles ".cnf" "" $ \problemPath _ -> do
+    withFile problemPath WriteMode $ \fh ->
+      hPutBuilder fh (dimacs problem)
+
+    (exit, out, _err) <-
+      readProcessWithExitCode path [problemPath] []
+
+    let sol = parseSolution5 out
+
+    return (resultOf exit, sol)
+
+parseSolution5 :: String -> IntMap Bool
+parseSolution5 txt = IntMap.fromList [(abs v, v > 0) | v <- vars, v /= 0]
+  where
+    vlines = [l | ('v':l) <- lines txt]
+    vars = map read (foldMap words vlines)
diff --git a/tests/Moore.hs b/tests/Moore.hs
--- a/tests/Moore.hs
+++ b/tests/Moore.hs
@@ -38,7 +38,7 @@
 
 mainf d k n s = do
   putStrLn $ unwords [ "degree <=", show d, "diameter <=", show k, "nodes ==", show n, "symmetry ==", show s ]
-  (s, mg) <- solveWith minisat $ moore d k n s
+  (s, mg) <- solveWith cryptominisat5 $ moore d k n s
   case (s, mg) of
      (Satisfied, Just g) -> do printA g ; return True
      _ -> do return False
diff --git a/tests/Speed.hs b/tests/Speed.hs
--- a/tests/Speed.hs
+++ b/tests/Speed.hs
@@ -14,7 +14,7 @@
 
 mainf n = do
   putStrLn $ unwords [ "n",  show n ]
-  (s, mgs) <- solveWith minisat $ do
+  (s, mgs) <- solveWith cryptominisat5 $ do
       gs <- replicateM n exists
       forM_ (zip gs $ tail gs) $ \ (x,y) -> assert ( x /== y )
       return (gs :: [Bit])
diff --git a/tests/Z001.hs b/tests/Z001.hs
--- a/tests/Z001.hs
+++ b/tests/Z001.hs
@@ -15,7 +15,7 @@
 import Control.Monad.State
 
 main = do
-  (Satisfied, Just ms) <- solveWith minisat $ do
+  (Satisfied, Just ms) <- solveWith cryptominisat5 $ do
     [ Restricted a, Restricted b ]
         :: [ Restricted 5 (NBV 3) ] <- replicateM 2 unknown
     -- assert $ gt (a^2 * b^2) (b^3 * a^3)