diff --git a/AUTHORS.md b/AUTHORS.md
--- a/AUTHORS.md
+++ b/AUTHORS.md
@@ -6,7 +6,7 @@
 
 It was revived by [Johan Kiviniemi](mailto:ersatz@johan.kiviniemi.name) [@ion1](https://github.com/ion1) who got it into a working condition by implementing some missing parts, which inspired the original author into polishing it up and releasing it.
 
-Eric Mertens (@glguy](https://github.com/glguy) has been pouring code into it ever since then.
+Eric Mertens [@glguy](https://github.com/glguy) has been pouring code into it ever since then.
 
 Omission from this page is by no means an attempt to discount your contributions! Thank you for all of your help!
 
diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,8 @@
+0.4.12 [2022.08.11]
+-------------------
+* Add `Equatable` and `Orderable` instances for more base and containers types
+* Add solver support for `z3`
+
 0.4.11 [2022.05.18]
 -------------------
 * Allow building with `mtl-2.3.*` and `transformers-0.6.*`.
diff --git a/ersatz.cabal b/ersatz.cabal
--- a/ersatz.cabal
+++ b/ersatz.cabal
@@ -1,5 +1,5 @@
 name:           ersatz
-version:        0.4.11
+version:        0.4.12
 license:        BSD3
 license-file:   LICENSE
 author:         Edward A. Kmett, Eric Mertens, Johan Kiviniemi
@@ -196,6 +196,7 @@
     Ersatz.Solver
     Ersatz.Solver.DepQBF
     Ersatz.Solver.Minisat
+    Ersatz.Solver.Z3
     Ersatz.Variable
     Ersatz.Counting
     Ersatz.Relation
diff --git a/src/Ersatz/Equatable.hs b/src/Ersatz/Equatable.hs
--- a/src/Ersatz/Equatable.hs
+++ b/src/Ersatz/Equatable.hs
@@ -24,10 +24,18 @@
 
 import Ersatz.Bit
 import GHC.Generics
+import Numeric.Natural
 import Data.IntMap (IntMap)
+import Data.Foldable (toList)
 import Data.Map (Map)
+import Data.Int
+import Data.Word
+import Data.Void
+import Data.List.NonEmpty (NonEmpty)
 import qualified Data.Map as Map
 import qualified Data.IntMap as IntMap
+import qualified Data.Sequence as Seq
+import qualified Data.Tree as Tree
 
 infix  4 ===, /==
 
@@ -57,6 +65,15 @@
     | IntMap.keys x == IntMap.keys y = IntMap.elems x === IntMap.elems y
     | otherwise                      = false
 
+instance Equatable v => Equatable (Seq.Seq v) where
+  x === y
+    | Seq.length x == Seq.length y = toList x === toList y
+    | otherwise                    = false
+
+-- manually written because ancient GHC didn't have the generics instance
+instance Equatable a => Equatable (Tree.Tree a) where
+  Tree.Node x xs === Tree.Node y ys = x === y && xs === ys
+
 instance (Equatable a, Equatable b) => Equatable (a,b)
 instance (Equatable a, Equatable b, Equatable c) => Equatable (a,b,c)
 instance (Equatable a, Equatable b, Equatable c, Equatable d) => Equatable (a,b,c,d)
@@ -65,6 +82,7 @@
 instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f, Equatable g) => Equatable (a,b,c,d,e,f,g)
 instance Equatable a => Equatable (Maybe a)
 instance Equatable a => Equatable [a]
+instance Equatable a => Equatable (NonEmpty a)
 instance (Equatable a, Equatable b) => Equatable (Either a b)
 
 class GEquatable f where
@@ -89,3 +107,25 @@
 
 instance Equatable a => GEquatable (K1 i a) where
   K1 a ===# K1 b = a === b
+
+-- Boring instances that end up being useful when deriving Equatable with Generics
+
+instance Equatable ()       where _ === _ = true
+instance Equatable Void     where x === y = x `seq` y `seq` error "Equatable[Void].==="
+instance Equatable Int      where x === y = bool (x == y)
+instance Equatable Integer  where x === y = bool (x == y)
+instance Equatable Natural  where x === y = bool (x == y)
+instance Equatable Word     where x === y = bool (x == y)
+instance Equatable Word8    where x === y = bool (x == y)
+instance Equatable Word16   where x === y = bool (x == y)
+instance Equatable Word32   where x === y = bool (x == y)
+instance Equatable Word64   where x === y = bool (x == y)
+instance Equatable Int8     where x === y = bool (x == y)
+instance Equatable Int16    where x === y = bool (x == y)
+instance Equatable Int32    where x === y = bool (x == y)
+instance Equatable Int64    where x === y = bool (x == y)
+instance Equatable Char     where x === y = bool (x == y)
+instance Equatable Float    where x === y = bool (x == y)
+instance Equatable Double   where x === y = bool (x == y)
+instance Equatable Ordering where x === y = bool (x == y)
+instance Equatable Bool     where x === y = bool (x == y)
diff --git a/src/Ersatz/Orderable.hs b/src/Ersatz/Orderable.hs
--- a/src/Ersatz/Orderable.hs
+++ b/src/Ersatz/Orderable.hs
@@ -25,9 +25,18 @@
 
 import Prelude hiding ((&&),(||),not,and,or,all,any)
 
+import Data.Foldable (toList)
+import Data.Int
+import Data.Void
+import Data.Word
 import Ersatz.Bit
 import Ersatz.Equatable
 import GHC.Generics
+import Numeric.Natural
+import qualified Data.IntMap as IntMap
+import qualified Data.Map as Map
+import qualified Data.Sequence as Seq
+import qualified Data.Tree as Tree
 
 infix  4 <?, <=?, >=?, >?
 
@@ -57,6 +66,44 @@
   a <?  b = not a && b
   a <=? b = not a || b
 
+-- | Compare by lexicographic order on sorted key-value pairs
+instance (Ord k, Orderable v) => Orderable (Map.Map k v) where
+  x <?  y = assocsLt (Map.assocs x) (Map.assocs y)
+  x <=? y = assocsLe (Map.assocs x) (Map.assocs y)
+
+-- | Compare by lexicographic order on sorted key-value pairs
+instance Orderable v => Orderable (IntMap.IntMap v) where
+  x <?  y = assocsLt (IntMap.assocs x) (IntMap.assocs y)
+  x <=? y = assocsLe (IntMap.assocs x) (IntMap.assocs y)
+
+assocsLt :: (Ord k, Orderable v) => [(k,v)] -> [(k,v)] -> Bit
+assocsLt _ [] = false
+assocsLt [] _ = true
+assocsLt ((k1,v1):xs) ((k2,v2):ys) =
+  case compare k1 k2 of
+    LT -> true
+    GT -> false
+    EQ -> v1 <? v2 || v1 === v2 && assocsLt xs ys
+
+assocsLe :: (Ord k, Orderable v) => [(k,v)] -> [(k,v)] -> Bit
+assocsLe [] _ = true
+assocsLe _ [] = false
+assocsLe ((k1,v1):xs) ((k2,v2):ys) =
+  case compare k1 k2 of
+    LT -> true
+    GT -> false
+    EQ -> v1 <? v2 || v1 === v2 && assocsLe xs ys
+
+-- | Compare by lexicographic order on elements
+instance Orderable v => Orderable (Seq.Seq v) where
+  x <?  y = toList x <?  toList y
+  x <=? y = toList x <=? toList y
+
+-- | Compare by lexicographic order on: root node, list of children
+instance Orderable a => Orderable (Tree.Tree a) where
+  Tree.Node x xs <?  Tree.Node y ys = (x,xs) <?  (y,ys)
+  Tree.Node x xs <=? Tree.Node y ys = (x,xs) <=? (y,ys)
+
 instance (Orderable a, Orderable b) => Orderable (a,b)
 instance (Orderable a, Orderable b, Orderable c) => Orderable (a,b,c)
 instance (Orderable a, Orderable b, Orderable c, Orderable d) => Orderable (a,b,c,d)
@@ -115,3 +162,44 @@
 instance Orderable a => GOrderable (K1 i a) where
   K1 a <?#  K1 b = a <?  b
   K1 a <=?# K1 b = a <=? b
+
+-- Boring instances that end up being useful when deriving Orderable with Generics
+
+instance Orderable ()       where _ <?  _ = false
+                                  _ <=? _ = true
+instance Orderable Void     where x <?  y = x `seq` y `seq` error "Orderable[Void].<?"
+                                  x <=? y = x `seq` y `seq` error "Orderable[Void].<=?"
+instance Orderable Int      where x <?  y = bool (x <  y)
+                                  x <=? y = bool (x <= y)
+instance Orderable Integer  where x <?  y = bool (x <  y)
+                                  x <=? y = bool (x <= y)
+instance Orderable Natural  where x <?  y = bool (x <  y)
+                                  x <=? y = bool (x <= y)
+instance Orderable Word     where x <?  y = bool (x <  y)
+                                  x <=? y = bool (x <= y)
+instance Orderable Word8    where x <?  y = bool (x <  y)
+                                  x <=? y = bool (x <= y)
+instance Orderable Word16   where x <?  y = bool (x <  y)
+                                  x <=? y = bool (x <= y)
+instance Orderable Word32   where x <?  y = bool (x <  y)
+                                  x <=? y = bool (x <= y)
+instance Orderable Word64   where x <?  y = bool (x <  y)
+                                  x <=? y = bool (x <= y)
+instance Orderable Int8     where x <?  y = bool (x <  y)
+                                  x <=? y = bool (x <= y)
+instance Orderable Int16    where x <?  y = bool (x <  y)
+                                  x <=? y = bool (x <= y)
+instance Orderable Int32    where x <?  y = bool (x <  y)
+                                  x <=? y = bool (x <= y)
+instance Orderable Int64    where x <?  y = bool (x <  y)
+                                  x <=? y = bool (x <= y)
+instance Orderable Char     where x <?  y = bool (x <  y)
+                                  x <=? y = bool (x <= y)
+instance Orderable Float    where x <?  y = bool (x <  y)
+                                  x <=? y = bool (x <= y)
+instance Orderable Double   where x <?  y = bool (x <  y)
+                                  x <=? y = bool (x <= y)
+instance Orderable Ordering where x <?  y = bool (x <  y)
+                                  x <=? y = bool (x <= y)
+instance Orderable Bool     where x <?  y = bool (x <  y)
+                                  x <=? y = bool (x <= y)
diff --git a/src/Ersatz/Solver.hs b/src/Ersatz/Solver.hs
--- a/src/Ersatz/Solver.hs
+++ b/src/Ersatz/Solver.hs
@@ -10,6 +10,7 @@
 module Ersatz.Solver
   ( module Ersatz.Solver.DepQBF
   , module Ersatz.Solver.Minisat
+  , module Ersatz.Solver.Z3
   , solveWith
   ) where
 
@@ -21,6 +22,7 @@
 import Ersatz.Solution
 import Ersatz.Solver.DepQBF
 import Ersatz.Solver.Minisat
+import Ersatz.Solver.Z3
 
 solveWith ::
   (Monad m, MonadPlus n, HasSAT s, Default s, Codec a) =>
diff --git a/src/Ersatz/Solver/Common.hs b/src/Ersatz/Solver/Common.hs
--- a/src/Ersatz/Solver/Common.hs
+++ b/src/Ersatz/Solver/Common.hs
@@ -14,14 +14,18 @@
   -- * Support for trying many solvers
   , trySolvers
   , NoSolvers(..)
+
+  , parseSolution5
   ) where
 
 import Control.Exception (Exception(..), throwIO)
 import Control.Monad.IO.Class
 import Ersatz.Solution
 import System.Exit (ExitCode(..))
-import System.IO.Error (isDoesNotExistError, tryIOError)
+import System.IO.Error (tryIOError)
 import System.IO.Temp (withSystemTempDirectory)
+import Data.IntMap (IntMap)
+import qualified Data.IntMap.Strict as IntMap
 
 withTempFiles :: MonadIO m
               => FilePath  -- ^ Problem file extension including the dot, if any
@@ -56,7 +60,11 @@
     runSolver solver next es =
       do res <- tryIOError (solver problem)
          case res of
-           Left e
-             | isDoesNotExistError e -> next (e:es)
-             | otherwise             -> ioError e
-           Right x                   -> return x
+           Left  e -> next (e:es)
+           Right x -> return x
+
+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/src/Ersatz/Solver/Minisat.hs b/src/Ersatz/Solver/Minisat.hs
--- a/src/Ersatz/Solver/Minisat.hs
+++ b/src/Ersatz/Solver/Minisat.hs
@@ -96,9 +96,3 @@
     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/src/Ersatz/Solver/Z3.hs b/src/Ersatz/Solver/Z3.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Solver/Z3.hs
@@ -0,0 +1,44 @@
+--------------------------------------------------------------------
+-- |
+-- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013
+-- License   :  BSD3
+-- Maintainer:  Edward Kmett <ekmett@gmail.com>
+-- Stability :  experimental
+-- Portability: non-portable
+--
+--------------------------------------------------------------------
+module Ersatz.Solver.Z3
+  ( z3
+  , z3Path
+  ) where
+
+import Data.ByteString.Builder
+import Control.Monad.IO.Class
+import Ersatz.Problem
+import Ersatz.Solution
+import Ersatz.Solver.Common
+import System.IO
+import System.Process (readProcessWithExitCode)
+
+-- | 'Solver' for 'SAT' problems that tries to invoke the @z3@ executable from the @PATH@
+z3 :: MonadIO m => Solver SAT m
+z3 = z3Path "z3"
+
+-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes @z3@ compatible arguments.
+--
+-- The 'FilePath' refers to the path to the executable.
+z3Path :: MonadIO m => FilePath -> Solver SAT m
+z3Path path problem = liftIO $
+  withTempFiles ".cnf" "" $ \problemPath _ -> do
+    withFile problemPath WriteMode $ \fh ->
+      hPutBuilder fh (dimacs problem)
+
+    (_exit, out, _err) <-
+      readProcessWithExitCode path ["-dimacs", problemPath] []
+
+    let result = case lines out of
+                    "s SATISFIABLE":_   -> Satisfied
+                    "s UNSATISFIABLE":_ -> Unsatisfied
+                    _                   -> Unsolved
+
+    return (result, parseSolution5 out)