From db7acb42729d7691bd915e3e81665169e18df835 Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Fri, 15 Jan 2021 17:07:05 -0800
Subject: [PATCH 01/17] [crux-llvm] Import reformatting in test.

---
 crux-llvm/test/Test.hs | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/crux-llvm/test/Test.hs b/crux-llvm/test/Test.hs
index db720abcd..d80af419d 100644
--- a/crux-llvm/test/Test.hs
+++ b/crux-llvm/test/Test.hs
@@ -2,22 +2,22 @@
 {-# LANGUAGE OverloadedStrings #-}
 module Main where
 
-import Control.Exception (bracket, SomeException, try)
+import           Control.Exception (bracket, SomeException, try)
 
-import GHC.IO.Handle (hDuplicate, hDuplicateTo)
+import           GHC.IO.Handle (hDuplicate, hDuplicateTo)
 
 import qualified Data.ByteString.Lazy as BSIO
-import Data.Char ( isLetter )
-import Data.List ( isInfixOf )
-import System.Directory( doesFileExist )
-import System.Environment ( withArgs, lookupEnv )
-import System.Exit ( ExitCode(..) )
-import System.FilePath (takeBaseName, replaceExtension)
-import System.IO --(IOMode(..), hFlush, withFile, stdout, stderr)
-import System.Process ( readProcess )
+import           Data.Char ( isLetter )
+import           Data.List ( isInfixOf )
+import           System.Directory ( doesFileExist )
+import           System.Environment ( withArgs, lookupEnv )
+import           System.Exit ( ExitCode(..) )
+import           System.FilePath (takeBaseName, replaceExtension)
+import           System.IO
+import           System.Process ( readProcess )
 
-import Test.Tasty (defaultMain, testGroup, TestTree)
-import Test.Tasty.Golden (goldenVsString, findByExtension)
+import           Test.Tasty (defaultMain, testGroup, TestTree)
+import           Test.Tasty.Golden (goldenVsString, findByExtension)
 
 import qualified Crux.Log as C
 import qualified CruxLLVMMain as C

From 3f60fd7a7e8f4a4037e746f58cc766a2e3c76773 Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Fri, 15 Jan 2021 17:08:09 -0800
Subject: [PATCH 02/17] [crux-llvm] Cleanup clang version detection in test.

---
 crux-llvm/test/Test.hs | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/crux-llvm/test/Test.hs b/crux-llvm/test/Test.hs
index d80af419d..a70b5fcc7 100644
--- a/crux-llvm/test/Test.hs
+++ b/crux-llvm/test/Test.hs
@@ -9,6 +9,7 @@ import           GHC.IO.Handle (hDuplicate, hDuplicateTo)
 import qualified Data.ByteString.Lazy as BSIO
 import           Data.Char ( isLetter )
 import           Data.List ( isInfixOf )
+import           Data.Maybe ( fromMaybe )
 import           System.Directory ( doesFileExist )
 import           System.Environment ( withArgs, lookupEnv )
 import           System.Exit ( ExitCode(..) )
@@ -24,21 +25,21 @@ import qualified CruxLLVMMain as C
 
 
 main :: IO ()
-main = do
+main = defaultMain =<< suite =<< getClangVersion
 
+
+getClangVersion :: IO String
+getClangVersion = do
   -- Determine which version of clang will be used for these tests.
   -- An exception (E.g. in the readProcess if clang is not found) will
   -- result in termination (test failure).  Uses partial 'head' but
   -- this is just tests, and failure is captured.
-  clangBin <- lookupEnv "CLANG" >>= \case
-    Just x -> return x
-    Nothing -> return "clang"
+  clangBin <- fromMaybe "clang" <$> lookupEnv "CLANG"
   let isVerLine = isInfixOf "clang version"
       dropLetter = dropWhile (all isLetter)
       getVer = head . dropLetter . words . head . filter isVerLine . lines
-  ver <- getVer <$> readProcess clangBin [ "--version" ] ""
+  getVer <$> readProcess clangBin [ "--version" ] ""
 
-  defaultMain =<< suite ver
 
 suite :: String -> IO TestTree
 suite clangVer =

From f7311277104de624b265d83e49001f3728f0831c Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Fri, 15 Jan 2021 22:07:27 -0800
Subject: [PATCH 03/17] [crux-llvm] Add .gitignore to to crux-llvm for test
 output files.

---
 crux-llvm/.gitignore | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 crux-llvm/.gitignore

diff --git a/crux-llvm/.gitignore b/crux-llvm/.gitignore
new file mode 100644
index 000000000..8e8a564e4
--- /dev/null
+++ b/crux-llvm/.gitignore
@@ -0,0 +1 @@
+**/test-data/golden/*.print_out

From 69001a166a127ee3801f632462fdb30918d2891f Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Fri, 15 Jan 2021 22:09:34 -0800
Subject: [PATCH 04/17] [crux-llvm] Remove unused redir function in test.

---
 crux-llvm/test/Test.hs | 19 -------------------
 1 file changed, 19 deletions(-)

diff --git a/crux-llvm/test/Test.hs b/crux-llvm/test/Test.hs
index a70b5fcc7..ae209cf3a 100644
--- a/crux-llvm/test/Test.hs
+++ b/crux-llvm/test/Test.hs
@@ -77,22 +77,3 @@ goldenTests dir =
     notHidden ('.' : _) = False
     notHidden _ = True
 
-redir :: Handle -> [Handle] -> IO a -> IO a
-redir _ [] act = act
-redir out (h:hs) act =
-  do hFlush h; hSetBuffering h NoBuffering; hSetBuffering out NoBuffering
-     --buf <- hGetBuffering h
-     let save =
-           do old <- hDuplicate h
-              hPutStrLn h "about to save"
-              hFlush out; hFlush old
-              hDuplicateTo out h
-              hPutStrLn h "saved"
-              return old
-         restore old =
-           do hFlush old; hFlush h
-              hPutStrLn h "about to restore"
-              hDuplicateTo old h
-              hPutStrLn h "restored"
-              --hSetBuffering h buf
-     bracket save restore (const $ redir out hs act)

From 6b1ba7283f3a2e7481cce4d764b220fa0c8d0fc6 Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Fri, 15 Jan 2021 22:10:43 -0800
Subject: [PATCH 05/17] [crux-llvm] add crux-llvm output dir to gitignore

---
 crux-llvm/.gitignore | 1 +
 1 file changed, 1 insertion(+)

diff --git a/crux-llvm/.gitignore b/crux-llvm/.gitignore
index 8e8a564e4..5b7bf7d3d 100644
--- a/crux-llvm/.gitignore
+++ b/crux-llvm/.gitignore
@@ -1 +1,2 @@
 **/test-data/golden/*.print_out
+results

From cbb20451e245fb082bda2b37fee536f5fece3c4a Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Fri, 15 Jan 2021 22:11:40 -0800
Subject: [PATCH 06/17] [crux-llvm] switch from tasty-golden to tasty-sugar for
 testing.

---
 crux-llvm/crux-llvm.cabal                     |   2 +-
 crux-llvm/test-data/golden/float-cast.print   |   0
 crux-llvm/test-data/golden/float-cast2.print  |   0
 crux-llvm/test-data/golden/funnel.print       |   0
 crux-llvm/test-data/golden/gcd-test.print     |   0
 crux-llvm/test-data/golden/hello.print        |   0
 crux-llvm/test-data/golden/hello2.print       |   0
 crux-llvm/test-data/golden/printing.print     |   0
 crux-llvm/test-data/golden/string.print       |   0
 crux-llvm/test-data/golden/string2.print      |   0
 crux-llvm/test-data/golden/strlen_test.print  |   0
 crux-llvm/test-data/golden/strlen_test2.print |   0
 crux-llvm/test-data/golden/uint-cast.print    |   0
 crux-llvm/test-data/golden/vector-cmp.print   |   0
 crux-llvm/test-data/golden/vector-gep.print   |   0
 .../test-data/golden/vector-select.print      |   0
 crux-llvm/test/Test.hs                        | 112 +++++++++++-------
 17 files changed, 67 insertions(+), 47 deletions(-)
 create mode 100644 crux-llvm/test-data/golden/float-cast.print
 create mode 100644 crux-llvm/test-data/golden/float-cast2.print
 create mode 100644 crux-llvm/test-data/golden/funnel.print
 create mode 100644 crux-llvm/test-data/golden/gcd-test.print
 create mode 100644 crux-llvm/test-data/golden/hello.print
 create mode 100644 crux-llvm/test-data/golden/hello2.print
 create mode 100644 crux-llvm/test-data/golden/printing.print
 create mode 100644 crux-llvm/test-data/golden/string.print
 create mode 100644 crux-llvm/test-data/golden/string2.print
 create mode 100644 crux-llvm/test-data/golden/strlen_test.print
 create mode 100644 crux-llvm/test-data/golden/strlen_test2.print
 create mode 100644 crux-llvm/test-data/golden/uint-cast.print
 create mode 100644 crux-llvm/test-data/golden/vector-cmp.print
 create mode 100644 crux-llvm/test-data/golden/vector-gep.print
 create mode 100644 crux-llvm/test-data/golden/vector-select.print

diff --git a/crux-llvm/crux-llvm.cabal b/crux-llvm/crux-llvm.cabal
index 0437edf07..7bae9096d 100644
--- a/crux-llvm/crux-llvm.cabal
+++ b/crux-llvm/crux-llvm.cabal
@@ -179,7 +179,7 @@ test-suite crux-llvm-test
                 QuickCheck,
                 tasty            >= 0.10,
                 tasty-hunit      >= 0.10,
-                tasty-golden     >= 2.3,
+                tasty-sugar      >= 1.0.0.0,
                 text,
                 what4
 
diff --git a/crux-llvm/test-data/golden/float-cast.print b/crux-llvm/test-data/golden/float-cast.print
new file mode 100644
index 000000000..e69de29bb
diff --git a/crux-llvm/test-data/golden/float-cast2.print b/crux-llvm/test-data/golden/float-cast2.print
new file mode 100644
index 000000000..e69de29bb
diff --git a/crux-llvm/test-data/golden/funnel.print b/crux-llvm/test-data/golden/funnel.print
new file mode 100644
index 000000000..e69de29bb
diff --git a/crux-llvm/test-data/golden/gcd-test.print b/crux-llvm/test-data/golden/gcd-test.print
new file mode 100644
index 000000000..e69de29bb
diff --git a/crux-llvm/test-data/golden/hello.print b/crux-llvm/test-data/golden/hello.print
new file mode 100644
index 000000000..e69de29bb
diff --git a/crux-llvm/test-data/golden/hello2.print b/crux-llvm/test-data/golden/hello2.print
new file mode 100644
index 000000000..e69de29bb
diff --git a/crux-llvm/test-data/golden/printing.print b/crux-llvm/test-data/golden/printing.print
new file mode 100644
index 000000000..e69de29bb
diff --git a/crux-llvm/test-data/golden/string.print b/crux-llvm/test-data/golden/string.print
new file mode 100644
index 000000000..e69de29bb
diff --git a/crux-llvm/test-data/golden/string2.print b/crux-llvm/test-data/golden/string2.print
new file mode 100644
index 000000000..e69de29bb
diff --git a/crux-llvm/test-data/golden/strlen_test.print b/crux-llvm/test-data/golden/strlen_test.print
new file mode 100644
index 000000000..e69de29bb
diff --git a/crux-llvm/test-data/golden/strlen_test2.print b/crux-llvm/test-data/golden/strlen_test2.print
new file mode 100644
index 000000000..e69de29bb
diff --git a/crux-llvm/test-data/golden/uint-cast.print b/crux-llvm/test-data/golden/uint-cast.print
new file mode 100644
index 000000000..e69de29bb
diff --git a/crux-llvm/test-data/golden/vector-cmp.print b/crux-llvm/test-data/golden/vector-cmp.print
new file mode 100644
index 000000000..e69de29bb
diff --git a/crux-llvm/test-data/golden/vector-gep.print b/crux-llvm/test-data/golden/vector-gep.print
new file mode 100644
index 000000000..e69de29bb
diff --git a/crux-llvm/test-data/golden/vector-select.print b/crux-llvm/test-data/golden/vector-select.print
new file mode 100644
index 000000000..e69de29bb
diff --git a/crux-llvm/test/Test.hs b/crux-llvm/test/Test.hs
index ae209cf3a..5dbd7d2c7 100644
--- a/crux-llvm/test/Test.hs
+++ b/crux-llvm/test/Test.hs
@@ -1,31 +1,50 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
-module Main where
-
-import           Control.Exception (bracket, SomeException, try)
 
-import           GHC.IO.Handle (hDuplicate, hDuplicateTo)
+module Main where
 
+import           Control.Exception ( SomeException, try )
 import qualified Data.ByteString.Lazy as BSIO
 import           Data.Char ( isLetter )
 import           Data.List ( isInfixOf )
-import           Data.Maybe ( fromMaybe )
-import           System.Directory ( doesFileExist )
+import           Data.Maybe ( catMaybes, fromMaybe )
+import           Numeric.Natural
 import           System.Environment ( withArgs, lookupEnv )
 import           System.Exit ( ExitCode(..) )
-import           System.FilePath (takeBaseName, replaceExtension)
+import           System.FilePath ( (-<.>) )
 import           System.IO
 import           System.Process ( readProcess )
 
-import           Test.Tasty (defaultMain, testGroup, TestTree)
-import           Test.Tasty.Golden (goldenVsString, findByExtension)
+import qualified Test.Tasty as TT
+import           Test.Tasty.HUnit ( (@=?), testCase )
+import qualified Test.Tasty.Sugar as TS
 
 import qualified Crux.Log as C
 import qualified CruxLLVMMain as C
 
 
+cCube, llCube :: TS.CUBE
+cCube = TS.mkCUBE { TS.inputDir = "test-data/golden"
+                  , TS.rootName = "*.c"
+                  , TS.expectedSuffix = "good"
+                  , TS.associatedNames = [ ("config", "config")
+                                         , ("stdio",  "print")
+                                         ]
+                  }
+
+llCube = cCube { TS.rootName = "*.ll" }
+
 main :: IO ()
-main = defaultMain =<< suite =<< getClangVersion
+main = do sweets <- concat <$> mapM TS.findSugar [cCube, llCube]
+          clangVer <- getClangVersion
+          tests <- TS.withSugarGroups sweets TT.testGroup mkTest
+
+          let ingredients = TT.includingOptions TS.sugarOptions :
+                            TS.sugarIngredients [cCube, llCube] <>
+                            TT.defaultIngredients
+          TT.defaultMainWithIngredients ingredients $
+            TT.testGroup "crux-llvm"
+            [ TT.testGroup ("clang " <> clangVer) $ tests ]
 
 
 getClangVersion :: IO String
@@ -41,39 +60,40 @@ getClangVersion = do
   getVer <$> readProcess clangBin [ "--version" ] ""
 
 
-suite :: String -> IO TestTree
-suite clangVer =
-  testGroup "crux-llvm" . pure . testGroup ("clang " <> clangVer) . pure <$> goldenTests "test-data/golden"
-
-
-goldenTests :: FilePath -> IO TestTree
-goldenTests dir =
-  do cFiles <- findByExtension [".c",".ll"] dir
-     return $
-       testGroup "Golden testing of crux-llvm"
-         [ goldenVsString (takeBaseName cFile) goodFile $
-           do ex <- doesFileExist configFile
-              let cfgargs = if ex then ["--config="++configFile] else []
-
-              r <- withArgs (["--solver=z3",cFile] ++ cfgargs) $
-                     withFile outFile WriteMode $ \h ->
-                       let cfg = C.OutputConfig False h h True in -- Quiet mode, don't print colors
-                       (let bss = BSIO.pack . fmap (toEnum . fromEnum) . show in \case
-                         Left e -> "*** Crux failed with exception: " <> bss (show (e :: SomeException)) <> "\n"
-                         Right (ExitFailure v) -> "*** Crux failed with non-zero result: " <> bss (show v) <> "\n"
-                         Right ExitSuccess -> "")
-                       <$>
-                       (try $ C.mainWithOutputConfig cfg)
-              (<> r) <$> BSIO.readFile outFile
-
-         | cFile <- cFiles
-         , notHidden cFile
-         , let goodFile = replaceExtension cFile ".good"
-         , let outFile = replaceExtension cFile ".out"
-         , let configFile = replaceExtension cFile ".config"
-         ]
-  where
-    notHidden "" = True
-    notHidden ('.' : _) = False
-    notHidden _ = True
-
+mkTest :: TS.Sweets -> Natural -> TS.Expectation -> IO TT.TestTree
+mkTest sweet _ expct =
+  let outFile = TS.expectedFile expct -<.> ".out"
+      tname = TS.rootBaseName sweet
+      runCruxName = tname <> " crux run"
+      printFName = outFile -<.> ".print_out"
+
+      runCrux = Just $ testCase runCruxName $ do
+        let cfargs = maybe [] (\c -> ["--config=" <> c]) $
+                     lookup "config" (TS.associated expct)
+            failureMsg = let bss = BSIO.pack . fmap (toEnum . fromEnum) . show in \case
+              Left e -> "*** Crux failed with exception: " <> bss (show (e :: SomeException)) <> "\n"
+              Right (ExitFailure v) -> "*** Crux failed with non-zero result: " <> bss (show v) <> "\n"
+              Right ExitSuccess -> ""
+        r <- withFile outFile WriteMode $ \h ->
+          failureMsg <$> (try $
+                          withArgs (["--solver=z3", TS.rootFile sweet] ++ cfargs) $
+                          -- Quiet mode, don't print colors
+                          C.mainWithOutputConfig (C.OutputConfig False h h True))
+        BSIO.writeFile printFName r
+
+      checkPrint =
+        let runTest s = testCase (tname <> " crux print") $
+                        do r <- BSIO.readFile printFName
+                           BSIO.readFile s >>= (@=? r)
+        in runTest <$> lookup "stdio" (TS.associated expct)
+
+      checkOutput = Just $ testCase (tname <> " crux output") $ do
+        good <- BSIO.readFile (TS.expectedFile expct)
+        (good @=?) =<< BSIO.readFile outFile
+
+  in return $ TT.testGroup (TS.rootBaseName sweet) $ catMaybes
+     [
+       runCrux
+     , TT.after TT.AllSucceed runCruxName <$> checkPrint
+     , TT.after TT.AllSucceed runCruxName <$> checkOutput
+     ]

From e0ec3a08a57037be4cf06627de4e8f09b4aea429 Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Sun, 17 Jan 2021 10:23:09 -0800
Subject: [PATCH 07/17] [crux-llvm] Update test output file and specification
 of quietness.

---
 crux-llvm/test/Test.hs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/crux-llvm/test/Test.hs b/crux-llvm/test/Test.hs
index 5dbd7d2c7..c272f2ba1 100644
--- a/crux-llvm/test/Test.hs
+++ b/crux-llvm/test/Test.hs
@@ -65,7 +65,7 @@ mkTest sweet _ expct =
   let outFile = TS.expectedFile expct -<.> ".out"
       tname = TS.rootBaseName sweet
       runCruxName = tname <> " crux run"
-      printFName = outFile -<.> ".print_out"
+      printFName = outFile -<.> ".print.out"
 
       runCrux = Just $ testCase runCruxName $ do
         let cfargs = maybe [] (\c -> ["--config=" <> c]) $
@@ -78,7 +78,8 @@ mkTest sweet _ expct =
           failureMsg <$> (try $
                           withArgs (["--solver=z3", TS.rootFile sweet] ++ cfargs) $
                           -- Quiet mode, don't print colors
-                          C.mainWithOutputConfig (C.OutputConfig False h h True))
+                          let quietMode = True in
+                          C.mainWithOutputConfig (C.OutputConfig False h h quietMode))
         BSIO.writeFile printFName r
 
       checkPrint =

From d26977fc8b0f0c6212c6e97f8e1fe7ba289e4df9 Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Sun, 17 Jan 2021 11:33:01 -0800
Subject: [PATCH 08/17] [crux-llvm] Parameterize tests over solvers; add Yices
 to existing Z3.

Some test inputs do not pass for Yices; expected files for these are
omitted in this commit so that those inputs are not tested.  After
this PR is merged, issues can be created for those non-passing Yices
situations with corresponding expected files provided in those issues.
---
 .../{float-cast.good => float-cast.z3.good}   |  0
 .../{float-cast2.good => float-cast2.z3.good} |  0
 ...strlen_test2.good => strlen_test2.z3.good} |  0
 ...rlen_test2.print => strlen_test2.z3.print} |  0
 crux-llvm/test/Test.hs                        | 20 +++++++++++++++----
 5 files changed, 16 insertions(+), 4 deletions(-)
 rename crux-llvm/test-data/golden/{float-cast.good => float-cast.z3.good} (100%)
 rename crux-llvm/test-data/golden/{float-cast2.good => float-cast2.z3.good} (100%)
 rename crux-llvm/test-data/golden/{strlen_test2.good => strlen_test2.z3.good} (100%)
 rename crux-llvm/test-data/golden/{strlen_test2.print => strlen_test2.z3.print} (100%)

diff --git a/crux-llvm/test-data/golden/float-cast.good b/crux-llvm/test-data/golden/float-cast.z3.good
similarity index 100%
rename from crux-llvm/test-data/golden/float-cast.good
rename to crux-llvm/test-data/golden/float-cast.z3.good
diff --git a/crux-llvm/test-data/golden/float-cast2.good b/crux-llvm/test-data/golden/float-cast2.z3.good
similarity index 100%
rename from crux-llvm/test-data/golden/float-cast2.good
rename to crux-llvm/test-data/golden/float-cast2.z3.good
diff --git a/crux-llvm/test-data/golden/strlen_test2.good b/crux-llvm/test-data/golden/strlen_test2.z3.good
similarity index 100%
rename from crux-llvm/test-data/golden/strlen_test2.good
rename to crux-llvm/test-data/golden/strlen_test2.z3.good
diff --git a/crux-llvm/test-data/golden/strlen_test2.print b/crux-llvm/test-data/golden/strlen_test2.z3.print
similarity index 100%
rename from crux-llvm/test-data/golden/strlen_test2.print
rename to crux-llvm/test-data/golden/strlen_test2.z3.print
diff --git a/crux-llvm/test/Test.hs b/crux-llvm/test/Test.hs
index c272f2ba1..6ccc55519 100644
--- a/crux-llvm/test/Test.hs
+++ b/crux-llvm/test/Test.hs
@@ -27,6 +27,7 @@ cCube, llCube :: TS.CUBE
 cCube = TS.mkCUBE { TS.inputDir = "test-data/golden"
                   , TS.rootName = "*.c"
                   , TS.expectedSuffix = "good"
+                  , TS.validParams = [ ("solver", Just ["z3", "yices"]) ]
                   , TS.associatedNames = [ ("config", "config")
                                          , ("stdio",  "print")
                                          ]
@@ -62,21 +63,32 @@ getClangVersion = do
 
 mkTest :: TS.Sweets -> Natural -> TS.Expectation -> IO TT.TestTree
 mkTest sweet _ expct =
-  let outFile = TS.expectedFile expct -<.> ".out"
+  let solver = maybe "z3"
+               (\case
+                 (TS.Explicit s) -> s
+                 (TS.Assumed  s) -> s
+                 TS.NotSpecified -> "z3")
+               $ lookup "solver" (TS.expParamsMatch expct)
+      outFile = TS.expectedFile expct -<.> ".out"
       tname = TS.rootBaseName sweet
       runCruxName = tname <> " crux run"
       printFName = outFile -<.> ".print.out"
 
       runCrux = Just $ testCase runCruxName $ do
-        let cfargs = maybe [] (\c -> ["--config=" <> c]) $
-                     lookup "config" (TS.associated expct)
+        let cfargs = catMaybes
+                     [
+                       ("--config=" <>) <$> lookup "config" (TS.associated expct)
+                     , Just $ "--solver=" <> solver
+                     , Just $ "--timeout=3"  -- fail if crucible cannot find a solution in 3 seconds
+                     , Just $ "--goal-timeout=4"  -- fail if solver cannot find a solution in 4 seconds
+                     ]
             failureMsg = let bss = BSIO.pack . fmap (toEnum . fromEnum) . show in \case
               Left e -> "*** Crux failed with exception: " <> bss (show (e :: SomeException)) <> "\n"
               Right (ExitFailure v) -> "*** Crux failed with non-zero result: " <> bss (show v) <> "\n"
               Right ExitSuccess -> ""
         r <- withFile outFile WriteMode $ \h ->
           failureMsg <$> (try $
-                          withArgs (["--solver=z3", TS.rootFile sweet] ++ cfargs) $
+                          withArgs (cfargs <> [TS.rootFile sweet]) $
                           -- Quiet mode, don't print colors
                           let quietMode = True in
                           C.mainWithOutputConfig (C.OutputConfig False h h quietMode))

From 9eefad74f88713e43a5afd8ccc6ce826183acaae Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Sun, 17 Jan 2021 14:46:18 -0800
Subject: [PATCH 09/17] [crux-llvm] Add CVC4 online verification to tests.

---
 .../test-data/golden/strlen_test2.cvc4.good   | 29 +++++++++++++++++++
 .../test-data/golden/strlen_test2.cvc4.print  |  0
 crux-llvm/test/Test.hs                        |  2 +-
 3 files changed, 30 insertions(+), 1 deletion(-)
 create mode 100644 crux-llvm/test-data/golden/strlen_test2.cvc4.good
 create mode 100644 crux-llvm/test-data/golden/strlen_test2.cvc4.print

diff --git a/crux-llvm/test-data/golden/strlen_test2.cvc4.good b/crux-llvm/test-data/golden/strlen_test2.cvc4.good
new file mode 100644
index 000000000..d40425602
--- /dev/null
+++ b/crux-llvm/test-data/golden/strlen_test2.cvc4.good
@@ -0,0 +1,29 @@
+i = 0
+string[(length - i) - 1] = ????
+i = 1
+string[(length - i) - 1] = ????
+i = 2
+string[(length - i) - 1] = ????
+i = 3
+string[(length - i) - 1] = ????
+i = 4
+string[(length - i) - 1] = ????
+i = 5
+string[(length - i) - 1] = ????
+i = 6
+string[(length - i) - 1] = ????
+i = 7
+string[(length - i) - 1] = ????
+i = 8
+string[(length - i) - 1] = ????
+i = 9
+string[(length - i) - 1] = ????
+i = 10
+string[(length - i) - 1] = ????
+i = 11
+string[(length - i) - 1] = ????
+i = 12
+string[(length - i) - 1] = ????
+i = 13
+string[(length - i) - 1] = ????
+[Crux] Overall status: Valid.
diff --git a/crux-llvm/test-data/golden/strlen_test2.cvc4.print b/crux-llvm/test-data/golden/strlen_test2.cvc4.print
new file mode 100644
index 000000000..e69de29bb
diff --git a/crux-llvm/test/Test.hs b/crux-llvm/test/Test.hs
index 6ccc55519..7f112490d 100644
--- a/crux-llvm/test/Test.hs
+++ b/crux-llvm/test/Test.hs
@@ -27,7 +27,7 @@ cCube, llCube :: TS.CUBE
 cCube = TS.mkCUBE { TS.inputDir = "test-data/golden"
                   , TS.rootName = "*.c"
                   , TS.expectedSuffix = "good"
-                  , TS.validParams = [ ("solver", Just ["z3", "yices"]) ]
+                  , TS.validParams = [ ("solver", Just ["z3", "yices", "cvc4" ]) ]
                   , TS.associatedNames = [ ("config", "config")
                                          , ("stdio",  "print")
                                          ]

From 3e741c42206e75a44589815c4219f7d5536f21bf Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Sun, 17 Jan 2021 14:47:15 -0800
Subject: [PATCH 10/17] [crux-llvm] Add solver version reporting to test output

---
 crux-llvm/test/Test.hs | 49 ++++++++++++++++++++++++++++++++++++------
 1 file changed, 42 insertions(+), 7 deletions(-)

diff --git a/crux-llvm/test/Test.hs b/crux-llvm/test/Test.hs
index 7f112490d..5ae624301 100644
--- a/crux-llvm/test/Test.hs
+++ b/crux-llvm/test/Test.hs
@@ -6,7 +6,7 @@ module Main where
 import           Control.Exception ( SomeException, try )
 import qualified Data.ByteString.Lazy as BSIO
 import           Data.Char ( isLetter )
-import           Data.List ( isInfixOf )
+import           Data.List ( isInfixOf, isPrefixOf )
 import           Data.Maybe ( catMaybes, fromMaybe )
 import           Numeric.Natural
 import           System.Environment ( withArgs, lookupEnv )
@@ -60,6 +60,31 @@ getClangVersion = do
       getVer = head . dropLetter . words . head . filter isVerLine . lines
   getVer <$> readProcess clangBin [ "--version" ] ""
 
+getZ3Version :: IO String
+getZ3Version =
+  let getVer inp = let w = words inp
+                   in if and [ length w > 2, head w == "Z3" ]
+                      then w !! 2 else "?"
+      -- example inp: "Z3 version 4.8.7 - 64 bit"
+  in getVer <$> readProcess "z3" [ "--version" ] ""
+
+getYicesVersion :: IO String
+getYicesVersion =
+  let getVer inp = let w = words inp
+                   in if and [ length w > 1, head w == "Yices" ]
+                      then w !! 1 else "?"
+      -- example inp: "Yices 2.6.1\nCopyright ..."
+  in getVer <$> readProcess "yices" [ "--version" ] ""
+
+getCVC4Version :: IO String
+getCVC4Version =
+  let getVer inp = let w = words inp
+                   in if and [ length w > 4
+                             , "This is CVC4 version" `isPrefixOf` inp
+                             ]
+                      then w !! 4 else "?"
+      -- example inp: "This is CVC4 version 1.8\ncompiled ..."
+  in getVer <$> readProcess "cvc4" [ "--version" ] ""
 
 mkTest :: TS.Sweets -> Natural -> TS.Expectation -> IO TT.TestTree
 mkTest sweet _ expct =
@@ -104,9 +129,19 @@ mkTest sweet _ expct =
         good <- BSIO.readFile (TS.expectedFile expct)
         (good @=?) =<< BSIO.readFile outFile
 
-  in return $ TT.testGroup (TS.rootBaseName sweet) $ catMaybes
-     [
-       runCrux
-     , TT.after TT.AllSucceed runCruxName <$> checkPrint
-     , TT.after TT.AllSucceed runCruxName <$> checkOutput
-     ]
+  in do
+    solverVer <- case solver of
+      "z3" -> ("z3-v" <>) <$> getZ3Version
+      "yices" -> ("yices-v" <>) <$> getYicesVersion
+      "cvc4" -> ("cvc4-v" <>) <$> getCVC4Version
+      _ -> return "unknown-solver-for-version"
+
+    return $
+      TT.testGroup solverVer
+      [ TT.testGroup (TS.rootBaseName sweet) $ catMaybes
+        [
+          runCrux
+        , TT.after TT.AllSucceed runCruxName <$> checkPrint
+        , TT.after TT.AllSucceed runCruxName <$> checkOutput
+        ]
+      ]

From c07c3bdc3d9642bf4129c396e30da148e5006913 Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Mon, 18 Jan 2021 10:14:25 -0800
Subject: [PATCH 11/17] [crux-llvm] add STP and Boolector solver tests.

---
 crux-llvm/crux-llvm.cabal                     |  2 +-
 crux-llvm/test-data/golden/funnel.stp.good    |  2 ++
 crux-llvm/test-data/golden/hello.stp.good     |  3 ++
 crux-llvm/test-data/golden/hello2.stp.good    |  3 ++
 crux-llvm/test-data/golden/string.stp.good    |  4 +++
 crux-llvm/test-data/golden/string2.stp.good   |  4 +++
 .../test-data/golden/strlen_test.stp.good     |  2 ++
 .../test-data/golden/strlen_test.stp.print    |  1 +
 .../golden/strlen_test2.boolector.good        | 29 +++++++++++++++++++
 ...en_test2.cvc4.print => strlen_test2.print} |  0
 .../test-data/golden/strlen_test2.z3.print    |  0
 crux-llvm/test-data/golden/uint-cast.stp.good |  6 ++++
 .../{vector-cmp.good => vector-cmp.z3.good}   |  0
 .../test-data/golden/vector-gep.stp.good      |  2 ++
 .../test-data/golden/vector-select.stp.good   |  3 ++
 crux-llvm/test/Test.hs                        | 23 +++++++++++++--
 16 files changed, 81 insertions(+), 3 deletions(-)
 create mode 100644 crux-llvm/test-data/golden/funnel.stp.good
 create mode 100644 crux-llvm/test-data/golden/hello.stp.good
 create mode 100644 crux-llvm/test-data/golden/hello2.stp.good
 create mode 100644 crux-llvm/test-data/golden/string.stp.good
 create mode 100644 crux-llvm/test-data/golden/string2.stp.good
 create mode 100644 crux-llvm/test-data/golden/strlen_test.stp.good
 create mode 100644 crux-llvm/test-data/golden/strlen_test.stp.print
 create mode 100644 crux-llvm/test-data/golden/strlen_test2.boolector.good
 rename crux-llvm/test-data/golden/{strlen_test2.cvc4.print => strlen_test2.print} (100%)
 delete mode 100644 crux-llvm/test-data/golden/strlen_test2.z3.print
 create mode 100644 crux-llvm/test-data/golden/uint-cast.stp.good
 rename crux-llvm/test-data/golden/{vector-cmp.good => vector-cmp.z3.good} (100%)
 create mode 100644 crux-llvm/test-data/golden/vector-gep.stp.good
 create mode 100644 crux-llvm/test-data/golden/vector-select.stp.good

diff --git a/crux-llvm/crux-llvm.cabal b/crux-llvm/crux-llvm.cabal
index 7bae9096d..56b3cf80d 100644
--- a/crux-llvm/crux-llvm.cabal
+++ b/crux-llvm/crux-llvm.cabal
@@ -179,7 +179,7 @@ test-suite crux-llvm-test
                 QuickCheck,
                 tasty            >= 0.10,
                 tasty-hunit      >= 0.10,
-                tasty-sugar      >= 1.0.0.0,
+                tasty-sugar      >= 1.0.1.0,
                 text,
                 what4
 
diff --git a/crux-llvm/test-data/golden/funnel.stp.good b/crux-llvm/test-data/golden/funnel.stp.good
new file mode 100644
index 000000000..28639d9c1
--- /dev/null
+++ b/crux-llvm/test-data/golden/funnel.stp.good
@@ -0,0 +1,2 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] user error (STP is not configured to produce UNSAT cores)
diff --git a/crux-llvm/test-data/golden/hello.stp.good b/crux-llvm/test-data/golden/hello.stp.good
new file mode 100644
index 000000000..7e54eeb86
--- /dev/null
+++ b/crux-llvm/test-data/golden/hello.stp.good
@@ -0,0 +1,3 @@
+[Crux] Goal timeout requested but not supported by STP
+Hello, world
+[Crux] Overall status: Valid.
diff --git a/crux-llvm/test-data/golden/hello2.stp.good b/crux-llvm/test-data/golden/hello2.stp.good
new file mode 100644
index 000000000..e84a02b19
--- /dev/null
+++ b/crux-llvm/test-data/golden/hello2.stp.good
@@ -0,0 +1,3 @@
+[Crux] Goal timeout requested but not supported by STP
+Hello again, world
+[Crux] Overall status: Valid.
diff --git a/crux-llvm/test-data/golden/string.stp.good b/crux-llvm/test-data/golden/string.stp.good
new file mode 100644
index 000000000..b8913f366
--- /dev/null
+++ b/crux-llvm/test-data/golden/string.stp.good
@@ -0,0 +1,4 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] SMTLIB backend does not support function types as first class.
+CallStack (from HasCallStack):
+  error, called at src/What4/Protocol/SMTLib2.hs:369:3 in what4-1.0.0.0.99-inplace:What4.Protocol.SMTLib2
diff --git a/crux-llvm/test-data/golden/string2.stp.good b/crux-llvm/test-data/golden/string2.stp.good
new file mode 100644
index 000000000..b8913f366
--- /dev/null
+++ b/crux-llvm/test-data/golden/string2.stp.good
@@ -0,0 +1,4 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] SMTLIB backend does not support function types as first class.
+CallStack (from HasCallStack):
+  error, called at src/What4/Protocol/SMTLib2.hs:369:3 in what4-1.0.0.0.99-inplace:What4.Protocol.SMTLib2
diff --git a/crux-llvm/test-data/golden/strlen_test.stp.good b/crux-llvm/test-data/golden/strlen_test.stp.good
new file mode 100644
index 000000000..28639d9c1
--- /dev/null
+++ b/crux-llvm/test-data/golden/strlen_test.stp.good
@@ -0,0 +1,2 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] user error (STP is not configured to produce UNSAT cores)
diff --git a/crux-llvm/test-data/golden/strlen_test.stp.print b/crux-llvm/test-data/golden/strlen_test.stp.print
new file mode 100644
index 000000000..74cbd1566
--- /dev/null
+++ b/crux-llvm/test-data/golden/strlen_test.stp.print
@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"
diff --git a/crux-llvm/test-data/golden/strlen_test2.boolector.good b/crux-llvm/test-data/golden/strlen_test2.boolector.good
new file mode 100644
index 000000000..d40425602
--- /dev/null
+++ b/crux-llvm/test-data/golden/strlen_test2.boolector.good
@@ -0,0 +1,29 @@
+i = 0
+string[(length - i) - 1] = ????
+i = 1
+string[(length - i) - 1] = ????
+i = 2
+string[(length - i) - 1] = ????
+i = 3
+string[(length - i) - 1] = ????
+i = 4
+string[(length - i) - 1] = ????
+i = 5
+string[(length - i) - 1] = ????
+i = 6
+string[(length - i) - 1] = ????
+i = 7
+string[(length - i) - 1] = ????
+i = 8
+string[(length - i) - 1] = ????
+i = 9
+string[(length - i) - 1] = ????
+i = 10
+string[(length - i) - 1] = ????
+i = 11
+string[(length - i) - 1] = ????
+i = 12
+string[(length - i) - 1] = ????
+i = 13
+string[(length - i) - 1] = ????
+[Crux] Overall status: Valid.
diff --git a/crux-llvm/test-data/golden/strlen_test2.cvc4.print b/crux-llvm/test-data/golden/strlen_test2.print
similarity index 100%
rename from crux-llvm/test-data/golden/strlen_test2.cvc4.print
rename to crux-llvm/test-data/golden/strlen_test2.print
diff --git a/crux-llvm/test-data/golden/strlen_test2.z3.print b/crux-llvm/test-data/golden/strlen_test2.z3.print
deleted file mode 100644
index e69de29bb..000000000
diff --git a/crux-llvm/test-data/golden/uint-cast.stp.good b/crux-llvm/test-data/golden/uint-cast.stp.good
new file mode 100644
index 000000000..f12e9e2fa
--- /dev/null
+++ b/crux-llvm/test-data/golden/uint-cast.stp.good
@@ -0,0 +1,6 @@
+[Crux] Goal timeout requested but not supported by STP
+bvZext 32 (bvSelect 0 8 cX@3:bv)
+bvZext 32 (bvSelect 8 8 cX@3:bv)
+bvZext 32 (bvSelect 16 8 cX@3:bv)
+bvZext 32 (bvSelect 24 8 cX@3:bv)
+[Crux] Overall status: Valid.
diff --git a/crux-llvm/test-data/golden/vector-cmp.good b/crux-llvm/test-data/golden/vector-cmp.z3.good
similarity index 100%
rename from crux-llvm/test-data/golden/vector-cmp.good
rename to crux-llvm/test-data/golden/vector-cmp.z3.good
diff --git a/crux-llvm/test-data/golden/vector-gep.stp.good b/crux-llvm/test-data/golden/vector-gep.stp.good
new file mode 100644
index 000000000..7a5513b4c
--- /dev/null
+++ b/crux-llvm/test-data/golden/vector-gep.stp.good
@@ -0,0 +1,2 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] Overall status: Valid.
diff --git a/crux-llvm/test-data/golden/vector-select.stp.good b/crux-llvm/test-data/golden/vector-select.stp.good
new file mode 100644
index 000000000..d1e50f197
--- /dev/null
+++ b/crux-llvm/test-data/golden/vector-select.stp.good
@@ -0,0 +1,3 @@
+[Crux] Goal timeout requested but not supported by STP
+0x1:[32]
+[Crux] Overall status: Valid.
diff --git a/crux-llvm/test/Test.hs b/crux-llvm/test/Test.hs
index 5ae624301..9cccad6cc 100644
--- a/crux-llvm/test/Test.hs
+++ b/crux-llvm/test/Test.hs
@@ -27,7 +27,7 @@ cCube, llCube :: TS.CUBE
 cCube = TS.mkCUBE { TS.inputDir = "test-data/golden"
                   , TS.rootName = "*.c"
                   , TS.expectedSuffix = "good"
-                  , TS.validParams = [ ("solver", Just ["z3", "yices", "cvc4" ]) ]
+                  , TS.validParams = [ ("solver", Just ["z3", "yices", "cvc4", "boolector", "stp" ]) ]
                   , TS.associatedNames = [ ("config", "config")
                                          , ("stdio",  "print")
                                          ]
@@ -76,6 +76,16 @@ getYicesVersion =
       -- example inp: "Yices 2.6.1\nCopyright ..."
   in getVer <$> readProcess "yices" [ "--version" ] ""
 
+getSTPVersion :: IO String
+getSTPVersion =
+  let getVer inp = let w = words inp
+                   in if and [ length w > 2
+                             , head w == "STP"
+                             , w !! 1 == "version" ]
+                         then w !! 2 else "?"
+      -- example inp: "STP version 2.3.3\n..."
+  in getVer <$> readProcess "stp" [ "--version" ] ""
+
 getCVC4Version :: IO String
 getCVC4Version =
   let getVer inp = let w = words inp
@@ -86,6 +96,13 @@ getCVC4Version =
       -- example inp: "This is CVC4 version 1.8\ncompiled ..."
   in getVer <$> readProcess "cvc4" [ "--version" ] ""
 
+getBoolectorVersion :: IO String
+getBoolectorVersion =
+  let getVer inp = let w = words inp
+                   in if not (null w) then head w else "?"
+      -- example inp: "3.2.1"
+  in getVer <$> readProcess "boolector" [ "--version" ] ""
+
 mkTest :: TS.Sweets -> Natural -> TS.Expectation -> IO TT.TestTree
 mkTest sweet _ expct =
   let solver = maybe "z3"
@@ -94,7 +111,7 @@ mkTest sweet _ expct =
                  (TS.Assumed  s) -> s
                  TS.NotSpecified -> "z3")
                $ lookup "solver" (TS.expParamsMatch expct)
-      outFile = TS.expectedFile expct -<.> ".out"
+      outFile = TS.expectedFile expct -<.> "." <> solver <> ".out"
       tname = TS.rootBaseName sweet
       runCruxName = tname <> " crux run"
       printFName = outFile -<.> ".print.out"
@@ -133,7 +150,9 @@ mkTest sweet _ expct =
     solverVer <- case solver of
       "z3" -> ("z3-v" <>) <$> getZ3Version
       "yices" -> ("yices-v" <>) <$> getYicesVersion
+      "stp" -> ("stp-v" <>) <$> getSTPVersion
       "cvc4" -> ("cvc4-v" <>) <$> getCVC4Version
+      "boolector" -> ("boolector-v" <>) <$> getBoolectorVersion
       _ -> return "unknown-solver-for-version"
 
     return $

From 6458a877ed57a9392e0fb44a3b3bbf8e1a8c8bbf Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Mon, 18 Jan 2021 10:58:09 -0800
Subject: [PATCH 12/17] [crux-llvm] More updates of expected output for
 boolector and stp tests.

---
 crux-llvm/test-data/golden/funnel.stp.print      |  1 +
 .../test-data/golden/gcd-test.boolector.good     |  3 +++
 .../test-data/golden/gcd-test.boolector.print    |  1 +
 crux-llvm/test-data/golden/gcd-test.stp.good     | 16 ++++++++++++++++
 crux-llvm/test-data/golden/gcd-test.stp.print    |  1 +
 crux-llvm/test-data/golden/printing.stp.good     |  7 +++++++
 crux-llvm/test-data/golden/string.stp.print      |  1 +
 crux-llvm/test-data/golden/string2.stp.print     |  1 +
 8 files changed, 31 insertions(+)
 create mode 100644 crux-llvm/test-data/golden/funnel.stp.print
 create mode 100644 crux-llvm/test-data/golden/gcd-test.boolector.good
 create mode 100644 crux-llvm/test-data/golden/gcd-test.boolector.print
 create mode 100644 crux-llvm/test-data/golden/gcd-test.stp.good
 create mode 100644 crux-llvm/test-data/golden/gcd-test.stp.print
 create mode 100644 crux-llvm/test-data/golden/printing.stp.good
 create mode 100644 crux-llvm/test-data/golden/string.stp.print
 create mode 100644 crux-llvm/test-data/golden/string2.stp.print

diff --git a/crux-llvm/test-data/golden/funnel.stp.print b/crux-llvm/test-data/golden/funnel.stp.print
new file mode 100644
index 000000000..74cbd1566
--- /dev/null
+++ b/crux-llvm/test-data/golden/funnel.stp.print
@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"
diff --git a/crux-llvm/test-data/golden/gcd-test.boolector.good b/crux-llvm/test-data/golden/gcd-test.boolector.good
new file mode 100644
index 000000000..1fdbf7425
--- /dev/null
+++ b/crux-llvm/test-data/golden/gcd-test.boolector.good
@@ -0,0 +1,3 @@
+[Crux] user error (Invalid solver configuration:
+boolector is not a valid online solver (expected yices, cvc4, z3, or stp)
+)
diff --git a/crux-llvm/test-data/golden/gcd-test.boolector.print b/crux-llvm/test-data/golden/gcd-test.boolector.print
new file mode 100644
index 000000000..74cbd1566
--- /dev/null
+++ b/crux-llvm/test-data/golden/gcd-test.boolector.print
@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"
diff --git a/crux-llvm/test-data/golden/gcd-test.stp.good b/crux-llvm/test-data/golden/gcd-test.stp.good
new file mode 100644
index 000000000..ec3becd51
--- /dev/null
+++ b/crux-llvm/test-data/golden/gcd-test.stp.good
@@ -0,0 +1,16 @@
+[Crux] Goal timeout requested but not supported by STP
+depth = 0
+depth = 1
+depth = 2
+depth = 3
+depth = 4
+depth = 5
+depth = 6
+depth = 7
+depth = 8
+depth = 9
+depth = 10
+depth = 11
+depth = 12
+????
+[Crux] user error (STP is not configured to produce UNSAT cores)
diff --git a/crux-llvm/test-data/golden/gcd-test.stp.print b/crux-llvm/test-data/golden/gcd-test.stp.print
new file mode 100644
index 000000000..74cbd1566
--- /dev/null
+++ b/crux-llvm/test-data/golden/gcd-test.stp.print
@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"
diff --git a/crux-llvm/test-data/golden/printing.stp.good b/crux-llvm/test-data/golden/printing.stp.good
new file mode 100644
index 000000000..48243a1c1
--- /dev/null
+++ b/crux-llvm/test-data/golden/printing.stp.good
@@ -0,0 +1,7 @@
+[Crux] Goal timeout requested but not supported by STP
+44
+4294967252
+2c
+2C
+--------------------------
+[Crux] Overall status: Valid.
diff --git a/crux-llvm/test-data/golden/string.stp.print b/crux-llvm/test-data/golden/string.stp.print
new file mode 100644
index 000000000..74cbd1566
--- /dev/null
+++ b/crux-llvm/test-data/golden/string.stp.print
@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"
diff --git a/crux-llvm/test-data/golden/string2.stp.print b/crux-llvm/test-data/golden/string2.stp.print
new file mode 100644
index 000000000..74cbd1566
--- /dev/null
+++ b/crux-llvm/test-data/golden/string2.stp.print
@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"

From a73784ae4142d3a279ab1efdefe8e18687a904ae Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Mon, 18 Jan 2021 11:04:53 -0800
Subject: [PATCH 13/17] [crux-llvm] add funptr tests.

---
 crux-llvm/test-data/golden/funptr.c         | 22 +++++++++++++++++++++
 crux-llvm/test-data/golden/funptr.good      |  1 +
 crux-llvm/test-data/golden/funptr.print     |  0
 crux-llvm/test-data/golden/funptr.stp.good  |  2 ++
 crux-llvm/test-data/golden/funptr.stp.print |  1 +
 5 files changed, 26 insertions(+)
 create mode 100644 crux-llvm/test-data/golden/funptr.c
 create mode 100644 crux-llvm/test-data/golden/funptr.good
 create mode 100644 crux-llvm/test-data/golden/funptr.print
 create mode 100644 crux-llvm/test-data/golden/funptr.stp.good
 create mode 100644 crux-llvm/test-data/golden/funptr.stp.print

diff --git a/crux-llvm/test-data/golden/funptr.c b/crux-llvm/test-data/golden/funptr.c
new file mode 100644
index 000000000..5d16cb875
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr.c
@@ -0,0 +1,22 @@
+#include <crucible.h>
+
+int f(void) {
+    return 42;
+}
+
+int g(void) {
+    return 99;
+}
+
+unsigned long int sel(int a) {
+    if (a < 10)
+        return (unsigned long int)(&f);
+    return (unsigned long int)(&g);
+}
+
+int main() {
+    int arg = 3;
+    int (*fptr)(void) = sel(arg);
+    check (fptr() == 42);
+    return 0;
+}
diff --git a/crux-llvm/test-data/golden/funptr.good b/crux-llvm/test-data/golden/funptr.good
new file mode 100644
index 000000000..9c7ea10d9
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr.good
@@ -0,0 +1 @@
+[Crux] Overall status: Valid.
diff --git a/crux-llvm/test-data/golden/funptr.print b/crux-llvm/test-data/golden/funptr.print
new file mode 100644
index 000000000..e69de29bb
diff --git a/crux-llvm/test-data/golden/funptr.stp.good b/crux-llvm/test-data/golden/funptr.stp.good
new file mode 100644
index 000000000..28639d9c1
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr.stp.good
@@ -0,0 +1,2 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] user error (STP is not configured to produce UNSAT cores)
diff --git a/crux-llvm/test-data/golden/funptr.stp.print b/crux-llvm/test-data/golden/funptr.stp.print
new file mode 100644
index 000000000..74cbd1566
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr.stp.print
@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"

From 68199a9a532fd5b5d8b9fd26a6015a2edadcc0a6 Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Mon, 18 Jan 2021 17:07:20 -0800
Subject: [PATCH 14/17] [crux-llvm] add funptr-fiddle tests

---
 crux-llvm/crux-llvm.cabal                     |  2 +-
 crux-llvm/test-data/golden/funptr-fiddle.c    | 22 +++++++++++++++++++
 crux-llvm/test-data/golden/funptr-fiddle.good | 16 ++++++++++++++
 .../test-data/golden/funptr-fiddle.print      |  1 +
 .../test-data/golden/funptr-fiddle.stp.good   |  2 ++
 .../test-data/golden/funptr-fiddle.stp.print  |  1 +
 6 files changed, 43 insertions(+), 1 deletion(-)
 create mode 100644 crux-llvm/test-data/golden/funptr-fiddle.c
 create mode 100644 crux-llvm/test-data/golden/funptr-fiddle.good
 create mode 100644 crux-llvm/test-data/golden/funptr-fiddle.print
 create mode 100644 crux-llvm/test-data/golden/funptr-fiddle.stp.good
 create mode 100644 crux-llvm/test-data/golden/funptr-fiddle.stp.print

diff --git a/crux-llvm/crux-llvm.cabal b/crux-llvm/crux-llvm.cabal
index 56b3cf80d..dcc595476 100644
--- a/crux-llvm/crux-llvm.cabal
+++ b/crux-llvm/crux-llvm.cabal
@@ -179,7 +179,7 @@ test-suite crux-llvm-test
                 QuickCheck,
                 tasty            >= 0.10,
                 tasty-hunit      >= 0.10,
-                tasty-sugar      >= 1.0.1.0,
+                tasty-sugar      > 1.0.1.0,
                 text,
                 what4
 
diff --git a/crux-llvm/test-data/golden/funptr-fiddle.c b/crux-llvm/test-data/golden/funptr-fiddle.c
new file mode 100644
index 000000000..33e9101a4
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr-fiddle.c
@@ -0,0 +1,22 @@
+#include <crucible.h>
+
+int f(void) {
+    return 42;
+}
+
+unsigned long int g(void) {
+    return 99;
+}
+
+unsigned long int sel(int a) {
+    if (a < 10)
+        return (unsigned long int)(&f) + 1;
+    return (unsigned long int)(&g) + 0;
+}
+
+int main() {
+    int arg = 3;
+    int (*fptr)(void) = sel(arg);
+    check (fptr() == 42);
+    return 0;
+}
diff --git a/crux-llvm/test-data/golden/funptr-fiddle.good b/crux-llvm/test-data/golden/funptr-fiddle.good
new file mode 100644
index 000000000..9e4c1b417
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr-fiddle.good
@@ -0,0 +1,16 @@
+[Crux] Counter example for /home/kquick/work/crux-sugar/crux-llvm/test-data/golden/funptr-fiddle.c:0:0: error: in sel
+Undefined behavior encountered
+Details:
+  Addition of an offset to a pointer resulted in a pointer to an address outside of the allocation
+[Crux] Found counterexample for verification goal
+/home/kquick/work/crux-sugar/crux-llvm/test-data/golden/funptr-fiddle.c:0:0: error: in sel
+Undefined behavior encountered
+Details:
+  Addition of an offset to a pointer resulted in a pointer to an address outside of the allocation
+  Pointer: (3, 0x0:[64])
+  Offset: 0x1:[64]
+  Reference: 
+    The C language standard, version C11
+    §6.5.6 Additive operators, ¶8
+    Document URL: http://www.iso-9899.info/n1570.html
+[Crux] Overall status: Invalid.
diff --git a/crux-llvm/test-data/golden/funptr-fiddle.print b/crux-llvm/test-data/golden/funptr-fiddle.print
new file mode 100644
index 000000000..8ceb6e844
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr-fiddle.print
@@ -0,0 +1 @@
+*** Crux failed with non-zero result: "1"
diff --git a/crux-llvm/test-data/golden/funptr-fiddle.stp.good b/crux-llvm/test-data/golden/funptr-fiddle.stp.good
new file mode 100644
index 000000000..28639d9c1
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr-fiddle.stp.good
@@ -0,0 +1,2 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] user error (STP is not configured to produce UNSAT cores)
diff --git a/crux-llvm/test-data/golden/funptr-fiddle.stp.print b/crux-llvm/test-data/golden/funptr-fiddle.stp.print
new file mode 100644
index 000000000..74cbd1566
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr-fiddle.stp.print
@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"

From bed3c68be5965b053a1c517f28d399e916bdc0f3 Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Mon, 18 Jan 2021 17:44:56 -0800
Subject: [PATCH 15/17] [crux-llvm] add more tests modifying function pointers.

---
 crux-llvm/test-data/golden/funptr-fiddle2.c   | 22 +++++++++++++++++++
 .../test-data/golden/funptr-fiddle2.good      | 11 ++++++++++
 .../test-data/golden/funptr-fiddle2.print     |  1 +
 .../test-data/golden/funptr-fiddle2.stp.good  |  2 ++
 .../test-data/golden/funptr-fiddle2.stp.print |  1 +
 crux-llvm/test-data/golden/funptr-fiddle3.c   | 22 +++++++++++++++++++
 .../test-data/golden/funptr-fiddle3.good      |  1 +
 .../test-data/golden/funptr-fiddle3.print     |  0
 .../test-data/golden/funptr-fiddle3.stp.good  |  2 ++
 .../test-data/golden/funptr-fiddle3.stp.print |  1 +
 10 files changed, 63 insertions(+)
 create mode 100644 crux-llvm/test-data/golden/funptr-fiddle2.c
 create mode 100644 crux-llvm/test-data/golden/funptr-fiddle2.good
 create mode 100644 crux-llvm/test-data/golden/funptr-fiddle2.print
 create mode 100644 crux-llvm/test-data/golden/funptr-fiddle2.stp.good
 create mode 100644 crux-llvm/test-data/golden/funptr-fiddle2.stp.print
 create mode 100644 crux-llvm/test-data/golden/funptr-fiddle3.c
 create mode 100644 crux-llvm/test-data/golden/funptr-fiddle3.good
 create mode 100644 crux-llvm/test-data/golden/funptr-fiddle3.print
 create mode 100644 crux-llvm/test-data/golden/funptr-fiddle3.stp.good
 create mode 100644 crux-llvm/test-data/golden/funptr-fiddle3.stp.print

diff --git a/crux-llvm/test-data/golden/funptr-fiddle2.c b/crux-llvm/test-data/golden/funptr-fiddle2.c
new file mode 100644
index 000000000..2fc08300c
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr-fiddle2.c
@@ -0,0 +1,22 @@
+#include <crucible.h>
+
+int f(void) {
+    return 42;
+}
+
+unsigned long int g(void) {
+    return 99;
+}
+
+unsigned long int sel(int a) {
+    if (a < 10)
+        return (unsigned long int)(&f) + 1 - 1;
+    return (unsigned long int)(&g) + 0;
+}
+
+int main() {
+    int arg = 3;
+    int (*fptr)(void) = sel(arg);
+    check ((fptr)() == 42);
+    return 0;
+}
diff --git a/crux-llvm/test-data/golden/funptr-fiddle2.good b/crux-llvm/test-data/golden/funptr-fiddle2.good
new file mode 100644
index 000000000..b4c022f19
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr-fiddle2.good
@@ -0,0 +1,11 @@
+[Crux] Counter example for /home/kquick/work/crux-sugar/crux-llvm/test-data/golden/funptr-fiddle2.c:0:0: error: in sel
+Error translating constant
+Illegal operation applied to pointer argument
+
+[Crux] Found counterexample for verification goal
+/home/kquick/work/crux-sugar/crux-llvm/test-data/golden/funptr-fiddle2.c:0:0: error: in sel
+Error translating constant
+Illegal operation applied to pointer argument
+
+
+[Crux] Overall status: Invalid.
diff --git a/crux-llvm/test-data/golden/funptr-fiddle2.print b/crux-llvm/test-data/golden/funptr-fiddle2.print
new file mode 100644
index 000000000..8ceb6e844
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr-fiddle2.print
@@ -0,0 +1 @@
+*** Crux failed with non-zero result: "1"
diff --git a/crux-llvm/test-data/golden/funptr-fiddle2.stp.good b/crux-llvm/test-data/golden/funptr-fiddle2.stp.good
new file mode 100644
index 000000000..28639d9c1
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr-fiddle2.stp.good
@@ -0,0 +1,2 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] user error (STP is not configured to produce UNSAT cores)
diff --git a/crux-llvm/test-data/golden/funptr-fiddle2.stp.print b/crux-llvm/test-data/golden/funptr-fiddle2.stp.print
new file mode 100644
index 000000000..74cbd1566
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr-fiddle2.stp.print
@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"
diff --git a/crux-llvm/test-data/golden/funptr-fiddle3.c b/crux-llvm/test-data/golden/funptr-fiddle3.c
new file mode 100644
index 000000000..e5b4b1722
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr-fiddle3.c
@@ -0,0 +1,22 @@
+#include <crucible.h>
+
+int f(void) {
+    return 42;
+}
+
+unsigned long int g(void) {
+    return 99;
+}
+
+unsigned long int sel(int a) {
+    if (a < 10)
+        return (unsigned long int)(&f) + 0;
+    return (unsigned long int)(&g) + 0;
+}
+
+int main() {
+    int arg = 3;
+    int (*fptr)(void) = sel(arg);
+    check ((fptr)() == 42);
+    return 0;
+}
diff --git a/crux-llvm/test-data/golden/funptr-fiddle3.good b/crux-llvm/test-data/golden/funptr-fiddle3.good
new file mode 100644
index 000000000..9c7ea10d9
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr-fiddle3.good
@@ -0,0 +1 @@
+[Crux] Overall status: Valid.
diff --git a/crux-llvm/test-data/golden/funptr-fiddle3.print b/crux-llvm/test-data/golden/funptr-fiddle3.print
new file mode 100644
index 000000000..e69de29bb
diff --git a/crux-llvm/test-data/golden/funptr-fiddle3.stp.good b/crux-llvm/test-data/golden/funptr-fiddle3.stp.good
new file mode 100644
index 000000000..28639d9c1
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr-fiddle3.stp.good
@@ -0,0 +1,2 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] user error (STP is not configured to produce UNSAT cores)
diff --git a/crux-llvm/test-data/golden/funptr-fiddle3.stp.print b/crux-llvm/test-data/golden/funptr-fiddle3.stp.print
new file mode 100644
index 000000000..74cbd1566
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr-fiddle3.stp.print
@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"

From bc24f8ff535e9629bc2da6493ac9e35291823af6 Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Mon, 18 Jan 2021 17:57:35 -0800
Subject: [PATCH 16/17] [crux-llvm] add funptr-array tests (see Issue #10)

---
 crux-llvm/test-data/golden/funptr-array.c     | 23 ++++++++++++
 crux-llvm/test-data/golden/funptr-array.good  | 36 +++++++++++++++++++
 crux-llvm/test-data/golden/funptr-array.print |  1 +
 .../test-data/golden/funptr-array.stp.good    |  2 ++
 .../test-data/golden/funptr-array.stp.print   |  1 +
 5 files changed, 63 insertions(+)
 create mode 100644 crux-llvm/test-data/golden/funptr-array.c
 create mode 100644 crux-llvm/test-data/golden/funptr-array.good
 create mode 100644 crux-llvm/test-data/golden/funptr-array.print
 create mode 100644 crux-llvm/test-data/golden/funptr-array.stp.good
 create mode 100644 crux-llvm/test-data/golden/funptr-array.stp.print

diff --git a/crux-llvm/test-data/golden/funptr-array.c b/crux-llvm/test-data/golden/funptr-array.c
new file mode 100644
index 000000000..4b5bbb534
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr-array.c
@@ -0,0 +1,23 @@
+/* See https://github.com/GaloisInc/crucible/issues/10 */
+
+#include <crucible.h>
+
+typedef int int_function(int);
+
+int succ(int x) { return x+1; }
+int pred(int x) { return x-1; }
+
+int mytestfunction(int i, int j) {
+    int_function *funs[] = { succ, pred };
+    return funs[i](j);
+}
+
+int main() {
+    int arg = __VERIFIER_nondet_int();
+    int v   = __VERIFIER_nondet_int();
+    int r;
+    assuming(arg >= 0 && arg <= 1);
+    r = mytestfunction(arg, v);
+    check (r == v + 1);
+    return 0;
+}
diff --git a/crux-llvm/test-data/golden/funptr-array.good b/crux-llvm/test-data/golden/funptr-array.good
new file mode 100644
index 000000000..168686dd6
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr-array.good
@@ -0,0 +1,36 @@
+[Crux] Counter example for /home/kquick/work/crux-sugar/crux-llvm/test-data/golden/funptr-array.c:12:12: error: in mytestfunction
+Failed to load function handle
+Details:
+  Cannot resolve a symbolic pointer to a function handle: (ite (eq 0x0:[64] (bvSum (bvMul 0x8:[64] (bvSext 64 cX@9:bv)))) 6 7, 0x0:[64])
+[Crux] Found counterexample for verification goal
+/home/kquick/work/crux-sugar/crux-llvm/test-data/golden/funptr-array.c:12:12: error: in mytestfunction
+Failed to load function handle
+Details:
+  Cannot resolve a symbolic pointer to a function handle: (ite (eq 0x0:[64] (bvSum (bvMul 0x8:[64] (bvSext 64 cX@9:bv)))) 6 7, 0x0:[64])
+  The given pointer could not be resolved to a callable function
+  Cannot resolve a symbolic pointer to a function handle: (ite (eq 0x0:[64] (bvSum (bvMul 0x8:[64] (bvSext 64 cX@9:bv)))) 6 7, 0x0:[64])
+  Attempting to load callable function with type: i32(i32)
+    Via pointer: (6, 0x0:[64])
+  In memory state:
+    Stack frame mytestfunction
+      No writes or allocations
+    Stack frame main
+      No writes or allocations
+    Base memory
+      Allocations:
+        GlobalAlloc 11 0x20:[64] Immutable 1-byte-aligned [global variable  ] .str
+        GlobalAlloc 10 0x10:[64] Immutable 16-byte-aligned [global variable  ] __const.mytestfunction.funs
+        GlobalAlloc 9 0x0:[64] Immutable 1-byte-aligned [defined function ] main
+        GlobalAlloc 8 0x0:[64] Immutable 1-byte-aligned [defined function ] mytestfunction
+        GlobalAlloc 7 0x0:[64] Immutable 1-byte-aligned [defined function ] pred
+        GlobalAlloc 6 0x0:[64] Immutable 1-byte-aligned [defined function ] succ
+        GlobalAlloc 5 0x0:[64] Immutable 1-byte-aligned [external function] crucible_assert
+        GlobalAlloc 4 0x0:[64] Immutable 1-byte-aligned [external function] crucible_assume
+        GlobalAlloc 3 0x0:[64] Immutable 1-byte-aligned [external function] __VERIFIER_nondet_int
+        GlobalAlloc 2 0x0:[64] Immutable 1-byte-aligned [external function] llvm.dbg.declare
+        GlobalAlloc 1 0x0:[64] Immutable 1-byte-aligned [external function] llvm.dbg.value
+      Writes:
+        Indexed chunk:
+          10 |->   *(10, 0x0:[64]) := [(6, 0x0:[64]),(7, 0x0:[64])]
+          11 |->   *(11, 0x0:[64]) := "test-data/golden/funptr-array.c\NUL"
+[Crux] Overall status: Invalid.
diff --git a/crux-llvm/test-data/golden/funptr-array.print b/crux-llvm/test-data/golden/funptr-array.print
new file mode 100644
index 000000000..8ceb6e844
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr-array.print
@@ -0,0 +1 @@
+*** Crux failed with non-zero result: "1"
diff --git a/crux-llvm/test-data/golden/funptr-array.stp.good b/crux-llvm/test-data/golden/funptr-array.stp.good
new file mode 100644
index 000000000..28639d9c1
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr-array.stp.good
@@ -0,0 +1,2 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] user error (STP is not configured to produce UNSAT cores)
diff --git a/crux-llvm/test-data/golden/funptr-array.stp.print b/crux-llvm/test-data/golden/funptr-array.stp.print
new file mode 100644
index 000000000..74cbd1566
--- /dev/null
+++ b/crux-llvm/test-data/golden/funptr-array.stp.print
@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"

From 22ec440390a9b85e69a8521b147c8563d1069689 Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Tue, 19 Jan 2021 11:01:40 -0800
Subject: [PATCH 17/17] [crux-llvm] do not fail if a solver is not present.

---
 crux-llvm/test/Test.hs | 92 ++++++++++++++++++++++++++++--------------
 1 file changed, 61 insertions(+), 31 deletions(-)

diff --git a/crux-llvm/test/Test.hs b/crux-llvm/test/Test.hs
index 9cccad6cc..3d34ee478 100644
--- a/crux-llvm/test/Test.hs
+++ b/crux-llvm/test/Test.hs
@@ -1,13 +1,15 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 module Main where
 
-import           Control.Exception ( SomeException, try )
+import           Control.Exception ( SomeException, catches, try, Handler(..), IOException )
 import qualified Data.ByteString.Lazy as BSIO
 import           Data.Char ( isLetter )
 import           Data.List ( isInfixOf, isPrefixOf )
 import           Data.Maybe ( catMaybes, fromMaybe )
+import qualified GHC.IO.Exception as GE
 import           Numeric.Natural
 import           System.Environment ( withArgs, lookupEnv )
 import           System.Exit ( ExitCode(..) )
@@ -57,51 +59,79 @@ getClangVersion = do
   clangBin <- fromMaybe "clang" <$> lookupEnv "CLANG"
   let isVerLine = isInfixOf "clang version"
       dropLetter = dropWhile (all isLetter)
-      getVer = head . dropLetter . words . head . filter isVerLine . lines
-  getVer <$> readProcess clangBin [ "--version" ] ""
+      getVer (Right inp) =
+        -- example inp: "clang version 10.0.1"
+        head $ dropLetter $ words $ head $ filter isVerLine $ lines inp
+      getVer (Left full) = full
+  getVer <$> readProcessVersion clangBin
 
 getZ3Version :: IO String
 getZ3Version =
-  let getVer inp = let w = words inp
-                   in if and [ length w > 2, head w == "Z3" ]
-                      then w !! 2 else "?"
-      -- example inp: "Z3 version 4.8.7 - 64 bit"
-  in getVer <$> readProcess "z3" [ "--version" ] ""
+  let getVer (Right inp) =
+        -- example inp: "Z3 version 4.8.7 - 64 bit"
+        let w = words inp
+        in if and [ length w > 2, head w == "Z3" ]
+           then w !! 2 else "?"
+      getVer (Left full) = full
+  in getVer <$> readProcessVersion "z3"
 
 getYicesVersion :: IO String
 getYicesVersion =
-  let getVer inp = let w = words inp
-                   in if and [ length w > 1, head w == "Yices" ]
-                      then w !! 1 else "?"
-      -- example inp: "Yices 2.6.1\nCopyright ..."
-  in getVer <$> readProcess "yices" [ "--version" ] ""
+  let getVer (Right inp) =
+        -- example inp: "Yices 2.6.1\nCopyright ..."
+        let w = words inp
+        in if and [ length w > 1, head w == "Yices" ]
+           then w !! 1 else "?"
+      getVer (Left full) = full
+  in getVer <$> readProcessVersion "yices"
 
 getSTPVersion :: IO String
 getSTPVersion =
-  let getVer inp = let w = words inp
-                   in if and [ length w > 2
-                             , head w == "STP"
-                             , w !! 1 == "version" ]
-                         then w !! 2 else "?"
-      -- example inp: "STP version 2.3.3\n..."
-  in getVer <$> readProcess "stp" [ "--version" ] ""
+  let getVer (Right inp) =
+        -- example inp: "STP version 2.3.3\n..."
+        let w = words inp
+        in if and [ length w > 2
+                  , head w == "STP"
+                  , w !! 1 == "version" ]
+           then w !! 2 else "?"
+      getVer (Left full) = full
+  in getVer <$> readProcessVersion "stp"
 
 getCVC4Version :: IO String
 getCVC4Version =
-  let getVer inp = let w = words inp
-                   in if and [ length w > 4
-                             , "This is CVC4 version" `isPrefixOf` inp
-                             ]
-                      then w !! 4 else "?"
-      -- example inp: "This is CVC4 version 1.8\ncompiled ..."
-  in getVer <$> readProcess "cvc4" [ "--version" ] ""
+  let getVer (Right inp) =
+        -- example inp: "This is CVC4 version 1.8\ncompiled ..."
+        let w = words inp
+        in if and [ length w > 4
+                  , "This is CVC4 version" `isPrefixOf` inp
+                  ]
+           then w !! 4 else "?"
+      getVer (Left full) = full
+  in getVer <$> readProcessVersion "cvc4"
 
 getBoolectorVersion :: IO String
 getBoolectorVersion =
-  let getVer inp = let w = words inp
-                   in if not (null w) then head w else "?"
-      -- example inp: "3.2.1"
-  in getVer <$> readProcess "boolector" [ "--version" ] ""
+  let getVer (Right inp) =
+        -- example inp: "3.2.1"
+        let w = words inp
+        in if not (null w) then head w else "?"
+      getVer (Left full) = full
+  in getVer <$> readProcessVersion "boolector"
+
+readProcessVersion :: String -> IO (Either String String)
+readProcessVersion forTool =
+  catches (Right <$> readProcess forTool [ "--version" ] "")
+  [ Handler $ \(e :: IOException) ->
+      if GE.ioe_type e == GE.NoSuchThing
+      then return $ Left "[missing]" -- tool executable not found
+      else do putStrLn $ "Warning: IO error attempting to determine " <> forTool <> " version:"
+              putStrLn $ show e
+              return $ Left "unknown"
+  , Handler $ \(e :: SomeException) -> do
+      putStrLn $ "Warning: error attempting to determine " <> forTool <> " version:"
+      putStrLn $ show e
+      return $ Left "??"
+  ]
 
 mkTest :: TS.Sweets -> Natural -> TS.Expectation -> IO TT.TestTree
 mkTest sweet _ expct =