diff --git a/.hlint.yaml b/.hlint.yaml
--- a/.hlint.yaml
+++ b/.hlint.yaml
@@ -7,3 +7,5 @@
     name: Use lambda-case
 
 - ignore: {name: Hoist not, within: [Ersatz.Bit]} # This is how we define `any`, ya dingus
+- ignore: {name: Use ||, within: [Ersatz.Relation.Prop]} # This is a different `or`
+- ignore: {name: Use &&, within: [Ersatz.Relation.Prop]} # This is a different `and`
diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,40 @@
+0.5 [2023.09.08]
+----------------
+* The `forall` function in `Ersatz.Variable` has been renamed to
+  `forall_`, since a future version of GHC will make the use of `forall` as an
+  identifier an error.
+* The types of `decode` and `solveWith` have been slightly less general:
+
+  ```diff
+  -decode :: MonadPlus f => Solution -> a -> f     (Decoded a)
+  +decode ::                Solution -> a -> Maybe (Decoded a)
+
+  -solveWith :: (Monad m, MonadPlus n, HasSAT s, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, n     (Decoded a))
+  +solveWith :: (Monad m,              HasSAT s, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))
+  ```
+
+  That is, these functions now use `Maybe` instead of an arbitrary `MonadPlus`.
+  This change came about because:
+
+  1. Practically all uses of `solveWith` in the wild are already picking `n` to
+     be `Maybe`, and
+  2. The behavior of `decode` and `solveWith` for `MonadPlus` instances besides
+     `Maybe` could  produce surprising results, as this behavior was not well
+     specified.
+* Fix a bug in which `decode` could return inconsistent results with solution
+  that underconstrain variables. For instance:
+
+  ```hs
+  do b <- exists
+     pure [b, not b]
+  ```
+
+  Previously, this could decode to `[False, False]` (an invalid assignment).
+  `ersatz` now adopts the convention that unconstrained non-negative `Literal`s
+  will always be assigned `False`, and unconstrained negative `Literal`s will
+  always be assigned `True`. This means that the example above would now decode
+  to `[False, True]`.
+
 0.4.13 [2022.11.01]
 -------------------
 * Make the examples compile with `mtl-2.3.*`.
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -46,7 +46,7 @@
 ```haskell
 verify_currying :: (MonadQSAT s m) => m ()
 verify_currying = do
-  (x::Bit, y::Bit, z::Bit) <- forall
+  (x::Bit, y::Bit, z::Bit) <- forall_
   assert $ ((x && y) ==> z) === (x ==> y ==> z)
 ```
 
diff --git a/ersatz.cabal b/ersatz.cabal
--- a/ersatz.cabal
+++ b/ersatz.cabal
@@ -1,5 +1,5 @@
 name:           ersatz
-version:        0.4.13
+version:        0.5
 license:        BSD3
 license-file:   LICENSE
 author:         Edward A. Kmett, Eric Mertens, Johan Kiviniemi
@@ -82,7 +82,9 @@
               , GHC == 8.8.4
               , GHC == 8.10.7
               , GHC == 9.0.2
-              , GHC == 9.2.2
+              , GHC == 9.2.7
+              , GHC == 9.4.5
+              , GHC == 9.6.2
 extra-source-files:
   .gitignore
   .hlint.yaml
@@ -168,7 +170,7 @@
   build-depends:
     array                >= 0.2      && < 0.6,
     base                 >= 4.9      && < 5,
-    bytestring           >= 0.10.4.0 && < 0.12,
+    bytestring           >= 0.10.4.0 && < 0.13,
     containers           >= 0.2.0.1  && < 0.7,
     data-default         >= 0.5      && < 0.8,
     lens                 >= 4        && < 6,
@@ -270,6 +272,21 @@
 --
 --   hs-source-dirs: tests
 --   Main-is: properties.hs
+
+test-suite hunit
+  type: exitcode-stdio-1.0
+  main-is: HUnit.hs
+  hs-source-dirs: tests
+  build-depends:
+    base,
+    containers,
+    data-default,
+    ersatz,
+    HUnit >= 1.2,
+    test-framework >= 0.6,
+    test-framework-hunit >= 0.2
+  default-language: Haskell2010
+  ghc-options: -Wall
 
 test-suite speed
   type: exitcode-stdio-1.0
diff --git a/src/Ersatz/Bit.hs b/src/Ersatz/Bit.hs
--- a/src/Ersatz/Bit.hs
+++ b/src/Ersatz/Bit.hs
@@ -27,7 +27,7 @@
 import qualified Prelude
 
 import Control.Applicative
-import Control.Monad (MonadPlus(..), liftM2, liftM3)
+import Control.Monad (liftM2, liftM3)
 import Data.Foldable (toList)
 import qualified Data.Foldable as Foldable
 import qualified Data.Traversable as Traversable
@@ -123,8 +123,7 @@
   type Decoded Bit = Bool
   encode = bool
   decode sol b
-      = maybe (pure False <|> pure True) pure $
-        solutionStableName sol (unsafePerformIO (makeStableName' b))
+      = solutionStableName sol (unsafePerformIO (makeStableName' b))
      -- The StableName didn’t have an associated literal with a solution,
      -- recurse to compute the value.
     <|> case b of
@@ -135,7 +134,9 @@
             decode sol $ if p then ct else cf
           Not c'  -> not <$> decode sol c'
           Var l   -> decode sol l
-          Run _ -> mzero
+          Run _ -> Nothing
+      -- If all else false, just return False.
+    <|> Just False
     where
       andMaybeBools :: [Maybe Bool] -> Maybe Bool
       andMaybeBools mbs
diff --git a/src/Ersatz/Codec.hs b/src/Ersatz/Codec.hs
--- a/src/Ersatz/Codec.hs
+++ b/src/Ersatz/Codec.hs
@@ -30,13 +30,23 @@
 -- | This class describes data types that can be marshaled to or from a SAT solver.
 class Codec a where
   type Decoded a :: Type
-  -- | Return a value based on the solution if one can be determined.
-  decode :: MonadPlus f => Solution -> a -> f (Decoded a)
+  -- | Return 'Just' a value based on the solution if one can be determined.
+  -- Otherwise, return 'Nothing'.
+  decode :: Solution -> a -> Maybe (Decoded a)
   encode :: Decoded a -> a
 
+-- | By convention, the 'decode' implementation will return 'False' for
+-- unconstrained non-negative 'Literal's and 'True' for unconstrained negative
+-- 'Literal's.
 instance Codec Literal where
   type Decoded Literal = Bool
-  decode s a = maybe (pure False <|> pure True) pure (solutionLiteral s a)
+  decode s a = case solutionLiteral s a of
+                 sol@(Just _) -> sol
+                 Nothing
+                   | i >= 0    -> Just False
+                   | otherwise -> Just True
+    where
+      i = literalId a
   encode True  = literalTrue
   encode False = literalFalse
 
diff --git a/src/Ersatz/Problem.hs b/src/Ersatz/Problem.hs
--- a/src/Ersatz/Problem.hs
+++ b/src/Ersatz/Problem.hs
@@ -53,6 +53,7 @@
 import Data.IntSet (IntSet)
 import qualified Data.IntSet as IntSet
 import qualified Data.List as List
+import qualified Data.List.NonEmpty as NE
 import Ersatz.Internal.Formula
 import Ersatz.Internal.Literal
 import Ersatz.Internal.StableName
@@ -247,12 +248,12 @@
                     , intDec (Seq.length tClauses)
                     ]
     quantified = foldMap go tQuantGroups
-      where go ls = bLine0 (q (head ls) : map (intDec . getQuant) ls)
+      where go ls = bLine0 (q (NE.head ls) : map (intDec . getQuant) (NE.toList ls))
             q Exists{} = char7 'e'
             q Forall{} = char7 'a'
     clauses = foldMap bClause tClauses
 
-    tQuantGroups = List.groupBy eqQuant (qdimacsQuantified t)
+    tQuantGroups = NE.groupBy eqQuant (qdimacsQuantified t)
       where
         eqQuant :: Quant -> Quant -> Bool
         eqQuant Exists{} Exists{} = True
@@ -311,9 +312,10 @@
   -- "Unbound atoms are to be considered as being existentially quantified in
   -- the first (i.e., the outermost) quantified set." per QDIMACS standard.
   -- Skip the implicit first existentials.
-  qdimacsQuantified q
-    | IntSet.null (q^.universals) = []
-    | otherwise = quants [head qUniversals..lastAtom'] qUniversals
+  qdimacsQuantified q =
+    case qUniversals of
+      []    -> []
+      (i:_) -> quants [i..lastAtom'] qUniversals
     where
       lastAtom'   = qdimacsNumVariables q
       qUniversals = IntSet.toAscList (q^.universals)
diff --git a/src/Ersatz/Solution.hs b/src/Ersatz/Solution.hs
--- a/src/Ersatz/Solution.hs
+++ b/src/Ersatz/Solution.hs
@@ -24,6 +24,9 @@
 
 data Solution = Solution
   { solutionLiteral    :: Literal -> Maybe Bool
+    -- ^ If a 'Literal' is uniquely assigned to a particular value, this will
+    -- return 'Just' of that value. If a 'Literal' is unconstrained (i.e., it
+    -- can be assigned either 'True' or 'False'), this will return 'Nothing'.
   , solutionStableName :: StableName () -> Maybe Bool
   }
 
diff --git a/src/Ersatz/Solver.hs b/src/Ersatz/Solver.hs
--- a/src/Ersatz/Solver.hs
+++ b/src/Ersatz/Solver.hs
@@ -14,7 +14,6 @@
   , solveWith
   ) where
 
-import Control.Monad
 import Control.Monad.State
 import Data.Default
 import Ersatz.Codec
@@ -24,9 +23,39 @@
 import Ersatz.Solver.Minisat
 import Ersatz.Solver.Z3
 
+-- | @'solveWith' solver prob@ solves a SAT problem @prob@ with the given
+-- @solver@. It returns a pair consisting of:
+--
+-- 1. A 'Result' that indicates if @prob@ is satisfiable ('Satisfied'),
+--    unsatisfiable ('Unsatisfied'), or if the solver could not determine any
+--    results ('Unsolved').
+--
+-- 2. A 'Decoded' answer that was decoded using the solution to @prob@. Note
+--    that this answer is only meaningful if the 'Result' is 'Satisfied' and
+--    the answer value is in a 'Just'.
+--
+-- Here is a small example of how to use 'solveWith':
+--
+-- @
+-- import Ersatz
+--
+-- main :: IO ()
+-- main = do
+--   res <- 'solveWith' minisat $ do
+--     (b1 :: Bit) <- exists
+--     (b2 :: Bit) <- exists
+--     assert (b1 === b2)
+--     pure [b1, b2]
+--   case res of
+--     (Satisfied, Just answer) -> print answer
+--     _ -> fail "Could not solve problem"
+-- @
+--
+-- Depending on the whims of @minisat@, this program may print either
+-- @[False, False]@ or @[True, True]@.
 solveWith ::
-  (Monad m, MonadPlus n, HasSAT s, Default s, Codec a) =>
-  Solver s m -> StateT s m a -> m (Result, n (Decoded a))
+  (Monad m, HasSAT s, Default s, Codec a) =>
+  Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))
 solveWith solver m = do
   (a, problem) <- runStateT m def
   (res, litMap) <- solver problem
diff --git a/src/Ersatz/Solver/DepQBF.hs b/src/Ersatz/Solver/DepQBF.hs
--- a/src/Ersatz/Solver/DepQBF.hs
+++ b/src/Ersatz/Solver/DepQBF.hs
@@ -32,6 +32,20 @@
 parseLiteral ('-':xs) = (read xs, False)
 parseLiteral xs = (read xs, True)
 
+-- Parse the QDIMACS output format, which is described in
+-- http://www.qbflib.org/qdimacs.html#output
+parseOutput :: String -> [(Int, Bool)]
+parseOutput out =
+  case lines out of
+    (_preamble:certLines) -> map parseCertLine certLines
+    [] -> error "QDIMACS output without preamble"
+  where
+    parseCertLine :: String -> (Int, Bool)
+    parseCertLine certLine =
+      case words certLine of
+        (_v:lit:_) -> parseLiteral lit
+        _ -> error $ "Malformed QDIMACS certificate line: " ++ certLine
+
 -- | This is a 'Solver' for 'QSAT' problems that lets you specify the path to the @depqbf@ executable.
 depqbfPath :: MonadIO m => FilePath -> Solver QSAT m
 depqbfPath path problem = liftIO $
@@ -47,6 +61,6 @@
     return $ (,) result $
       case result of
         Satisfied ->
-          I.fromList $ map (parseLiteral . head . tail . words) $ tail $ lines out
+          I.fromList $ parseOutput out
         _ ->
           I.empty
diff --git a/src/Ersatz/Variable.hs b/src/Ersatz/Variable.hs
--- a/src/Ersatz/Variable.hs
+++ b/src/Ersatz/Variable.hs
@@ -15,7 +15,7 @@
 module Ersatz.Variable
   ( Variable(..)
 #ifndef HLINT
-  , forall
+  , forall_
 #endif
   , exists
 
@@ -32,8 +32,8 @@
 exists = literally literalExists
 
 #ifndef HLINT
-forall :: (Variable a, MonadQSAT s m)  => m a
-forall = literally literalForall
+forall_ :: (Variable a, MonadQSAT s m) => m a
+forall_ = literally literalForall
 #endif
 
 class GVariable f where
diff --git a/tests/HUnit.hs b/tests/HUnit.hs
new file mode 100644
--- /dev/null
+++ b/tests/HUnit.hs
@@ -0,0 +1,38 @@
+-- | @HUnit@-based unit tests for @ersatz@.
+module Main where
+
+import Prelude hiding ((||), (&&), not)
+
+import Data.Default
+import qualified Data.IntMap.Strict as IntMap
+
+import Test.Framework
+import Test.Framework.Providers.HUnit
+import Test.HUnit (Assertion, (@?=))
+
+import Ersatz
+import Ersatz.Internal.Literal
+
+main :: IO ()
+main = defaultMain tests
+
+tests :: [Test]
+tests =
+  [ testGroup "unit tests"
+      [ testCase "unconstrained literals" case_unconstrained_literals
+      ]
+  ]
+
+-- A regression test for #60 and #76.
+case_unconstrained_literals :: Assertion
+case_unconstrained_literals =
+    decode sol [b1, not b1, b2, not b2, b1 || b2, b1 && b2] @?=
+      Just [False, True, False, True, False, False]
+      -- There are other valid answers, but in practice, ersatz will choose this
+      -- one due to the convention that the Codec Literal instance always
+      -- assigns non-negative unconstrained Literals to False and negative
+      -- unconstrained Literals to True.
+  where
+    sol = solutionFrom (IntMap.fromList [(1, True)]) (def :: SAT)
+    b1 = Var $ Literal 2
+    b2 = Var $ Literal 3
diff --git a/tests/Speed.hs b/tests/Speed.hs
--- a/tests/Speed.hs
+++ b/tests/Speed.hs
@@ -16,8 +16,12 @@
   putStrLn $ unwords [ "n",  show n ]
   (s, mgs) <- solveWith anyminisat $ do
       gs <- replicateM n exists
-      forM_ (zip gs $ tail gs) $ \ (x,y) -> assert ( x /== y )
+      forM_ (zipTail gs) $ \ (x,y) -> assert ( x /== y )
       return (gs :: [Bit])
   case (s, mgs) of
      (Satisfied, Just gs) -> do print $ length $ filter id gs
      _ -> do return ()
+
+zipTail :: [a] -> [(a, a)]
+zipTail []         = []
+zipTail xss@(_:xs) = zip xss xs
diff --git a/tests/Z001.hs b/tests/Z001.hs
--- a/tests/Z001.hs
+++ b/tests/Z001.hs
@@ -41,6 +41,8 @@
   unknown :: MonadSAT s m => m a
 
 -- | square matrices
+--
+-- Invariant: @dim >= 2@
 newtype Matrix (dim::Nat)  a = Matrix [[a]]
   deriving ( Show, Equatable, Orderable )
 
@@ -68,9 +70,33 @@
 
 for = flip map
 
-topleft (Matrix xss) = head (head xss)
-botright (Matrix xss) = last (last xss)
-topright (Matrix xss) = last (head xss)
+topleft (Matrix xss) =
+  case xss of
+    ((x:_):_) -> x
+    _ -> matrixInvariantViolated
+
+botright (Matrix xss)
+  | Just (_, xs) <- unsnoc xss
+  , Just (_, x)  <- unsnoc xs
+  = x
+  | otherwise
+  = matrixInvariantViolated
+
+topright (Matrix xss)
+  | xs:_ <- xss
+  , Just (_, x) <- unsnoc xs
+  = x
+  | otherwise
+  = matrixInvariantViolated
+
+unsnoc :: [a] -> Maybe ([a], a)
+unsnoc []     = Nothing
+unsnoc (x:xs) = case unsnoc xs of
+                  Nothing    -> Just ([], x)
+                  Just (a,b) -> Just (x:a, b)
+
+matrixInvariantViolated :: a
+matrixInvariantViolated = error "Matrix invariant violated"
 
 monotone m = positive (topleft m) && positive (botright m)