Haskell program repeatedly calling sat from the SBV library with an increasing number of variables

main.hs

import System.Environment (getArgs)
import Control.Monad (unless)
import Data.SBV

testInt :: Int -> Predicate
testInt n = do
        vars <- mkExistVars n
        let s = sum vars
        return $ s .>= (1::SInteger) &&& s .<= 5 &&& s ./= 3

testRun :: Int -> Int -> IO ()
testRun n i = do
        putStrLn $ "Test run " ++ show i
        result <- sat $ testInt n
        unless (modelExists result) (error "Predicate should be satisfiable")

testVars :: Int -> IO ()
testVars n = do
        putStrLn $ "Test with n = " ++ show n
        mapM_ (testRun n) [0..10]

main :: IO ()
main = do
        args <- getArgs
        let maxN = read $ head args
        mapM_ testVars [1..maxN]