diff --git a/executable/Main.hs b/executable/Main.hs
--- a/executable/Main.hs
+++ b/executable/Main.hs
@@ -32,7 +32,12 @@
     ["help"] -> help
     ["--help"] -> help
     ["--version"] ->
-      putStrLn $ "Jukebox version " ++ VERSION_jukebox
+      putStrLn $ "Jukebox version " ++
+#ifdef VERSION_jukebox
+      VERSION_jukebox
+#else
+      "unknown"
+#endif
     (('-':_):_) -> usage "Expected a tool name as first argument"
     (arg:args) ->
       case [tool | tool <- tools, name tool == arg] of
diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.4.2
+Version: 0.4.3
 Cabal-version: >= 1.8
 Build-type: Simple
 Author: Nick Smallbone
@@ -19,10 +19,6 @@
 License-file: LICENSE
 extra-source-files: src/errors.h gcc-static-libstdc++
 
-flag minisat
-  Description: Use minisat. Required for monotonicity inference.
-  Default: True
-
 flag static-cxx
   description: Build a binary which statically links against libstdc++.
   default: False
@@ -33,21 +29,10 @@
 
 Library
   Build-depends: base >= 4 && < 5, array, transformers >= 0.4.0.0, directory,
-    filepath, pretty >= 1.1.2.0, symbol, dlist, process, containers, uglymemo
+    filepath, pretty >= 1.1.2.0, symbol, dlist, process, containers, uglymemo,
+    minisat
   if !impl(ghc >= 8.0)
-    Build-depends: semigroups
-  if impl(ghc >= 8.6)
-    extensions: NoMonadFailDesugaring
-  if flag(minisat)
-    Build-depends: minisat
-    Exposed-modules:
-      Jukebox.Sat
-      Jukebox.Sat.ThreeValued
-      Jukebox.Sat.Equality
-      Jukebox.Sat.Minimise
-      Jukebox.Sat.Easy
-  else
-    cpp-options: -DNO_MINISAT
+    Build-depends: semigroups, fail
   ghc-options: -W -fno-warn-incomplete-patterns
   Build-tools: alex
   Hs-source-dirs: src
@@ -58,6 +43,11 @@
     Jukebox.Options
     Jukebox.ExternalProvers.E
     Jukebox.ExternalProvers.SPASS
+    Jukebox.Sat
+    Jukebox.Sat.ThreeValued
+    Jukebox.Sat.Equality
+    Jukebox.Sat.Minimise
+    Jukebox.Sat.Easy
     Jukebox.SMTLIB
     Jukebox.Toolbox
     Jukebox.Tools.Clausify
diff --git a/src/Jukebox/Sat/Easy.hs b/src/Jukebox/Sat/Easy.hs
--- a/src/Jukebox/Sat/Easy.hs
+++ b/src/Jukebox/Sat/Easy.hs
@@ -77,7 +77,7 @@
 modelValue x = do
   s <- Sat1 ask
   l <- var x
-  Just b <- liftIO (MiniSat.modelValue s l)
+  ~(Just b) <- liftIO (MiniSat.modelValue s l)
   return b
 
 addForm :: Ord a => Form a -> Sat1 a ()
diff --git a/src/Jukebox/TPTP/Parsec.hs b/src/Jukebox/TPTP/Parsec.hs
--- a/src/Jukebox/TPTP/Parsec.hs
+++ b/src/Jukebox/TPTP/Parsec.hs
@@ -1,10 +1,11 @@
-{-# LANGUAGE RankNTypes, BangPatterns, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances, TypeFamilies #-}
+{-# LANGUAGE RankNTypes, BangPatterns, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances, TypeFamilies, CPP #-}
 {-# OPTIONS_GHC -funfolding-creation-threshold=10000 -funfolding-use-threshold=10000 #-}
 module Jukebox.TPTP.Parsec where
 
 import Control.Applicative
 import Control.Monad
 import Data.List
+import Control.Monad.Fail
 
 -- Parser type and monad instances
 
@@ -35,6 +36,13 @@
   return x = Parsec (\ok err inp exp -> ok x err inp exp)
   {-# INLINE (>>=) #-}
   x >>= f = Parsec (\ok err inp exp  -> runParsec x (\y err inp exp -> runParsec (f y) ok err inp exp) err inp exp)
+
+#if __GLASGOW_HASKELL__ < 808
+  {-# INLINE fail #-}
+  fail _ = parseError []
+#endif
+
+instance MonadFail (Parsec a) where
   {-# INLINE fail #-}
   fail _ = parseError []