diff --git a/shake-ats.cabal b/shake-ats.cabal
--- a/shake-ats.cabal
+++ b/shake-ats.cabal
@@ -1,6 +1,6 @@
 cabal-version: 1.18
 name: shake-ats
-version: 1.6.0.2
+version: 1.8.0.0
 license: BSD3
 license-file: LICENSE
 copyright: Copyright: (c) 2018 Vanessa McHale
@@ -39,7 +39,7 @@
         base >=4.11 && <5,
         hashable -any,
         language-ats -any,
-        shake-ext >=2.8.0.0,
+        shake-ext >=2.9.0.0,
         hs2ats >=0.2.0.1,
         directory -any,
         microlens -any,
diff --git a/src/Development/Shake/ATS.hs b/src/Development/Shake/ATS.hs
--- a/src/Development/Shake/ATS.hs
+++ b/src/Development/Shake/ATS.hs
@@ -28,6 +28,7 @@
                              , ArtifactType (..)
                              , ATSGen (..)
                              , HATSGen (..)
+                             , Solver (..)
                              -- * Lenses
                              , atsTarget
                              , cFlags
@@ -48,6 +49,8 @@
                              , toolConfig
                              , cpphs
                              , hsFile
+                             , strip
+                             , solver
                              ) where
 
 import           Control.Arrow
@@ -80,8 +83,11 @@
     path <- liftIO $ getEnv "PATH"
     let env = patsEnv tc path
         patsc = patsopt tc
+        f = case (_solver tc) of
+                Ignore -> ("--constraint-ignore":)
+                _      -> id
 
-    command env patsc ["--output", out, "-dd", sourceFile, "-cc"]
+    command env patsc (f ["--output", out, "-dd", sourceFile, "-cc"])
 
 -- | Filter any generated errors with @pats-filter@.
 withPF :: Action (Exit, Stderr String, Stdout String) -- ^ Result of a 'cmd' or 'command'
@@ -100,7 +106,7 @@
 -- Copy source files to the appropriate place. This is necessary because
 -- @#include@s in ATS are weird.
 copySources :: ATSToolConfig -> [FilePath] -> Action ()
-copySources (ATSToolConfig home' _ _ _ _) sources =
+copySources (ATSToolConfig home' _ _ _ _ _) sources =
     forM_ sources $ \dep -> do
         liftIO $ createDirectoryIfMissing True (home' ++ "/" ++ takeDirectory dep)
         liftIO $ copyFile dep (home' ++ "/" ++ dep)
@@ -136,15 +142,15 @@
     let h = _patsHome tc
     let cc' = _cc tc
     h' <- pkgHome cc'
+    -- FIXME only bother with atslib if it's unnecessary?
     let libs'' = ("atslib" :) $ bool libs' ("gc" : libs') gc'
-    -- TODO only include /ccomp/atslib/lib if it's not a cross build
     pure $ CConfig [h ++ "/ccomp/runtime/", h, h' ++ "include", ".atspkg/contrib"] libs'' [h' ++ "lib", _patsHome tc ++ "/ccomp/atslib/lib"] extras (_linkStatic tc)
 
 patsEnv :: ATSToolConfig -> FilePath -> [CmdOption]
 patsEnv cfg path = EchoStderr False :
     zipWith AddEnv
-        ["PATSHOME", "PATH", "PATSHOMELOCS"]
-        [_patsHome cfg, _patsHome cfg ++ "/bin:" ++ path, _patsHomeLocs cfg]
+        ["PATSHOME", "PATH", "PATSHOMELOCS", "LIBGMP"]
+        [_patsHome cfg, _patsHome cfg ++ "/bin:" ++ path, _patsHomeLocs cfg ]
 
 atsToC :: FilePath -> FilePath
 atsToC = (-<.> "c") . (".atspkg/c/" <>)
@@ -164,6 +170,8 @@
 satsGen :: HATSGen -> Rules ()
 satsGen (HATSGen x y) = genLinks x y
 
+-- /.atspkg/contrib/atscntrb-hx-libgmp
+
 -- | Rules for generating binaries or libraries from ATS code. This is very
 -- general; use 'defaultATSTarget' for sensible defaults that can be modified
 -- with the provided lenses.
@@ -203,6 +211,7 @@
         cconfig'' <- cconfig _toolConfig _libs _gc (makeCFlags _cFlags _hsLibs ghcV' _gc)
 
         unit $ g _tgtType (_cc _toolConfig) (h' cTargets) _binTarget cconfig''
+        bool (pure ()) (stripA _binTarget (_cc _toolConfig)) _strip
 
 -- | Generate C code from ATS code.
 cgen :: ATSToolConfig
diff --git a/src/Development/Shake/ATS/Type.hs b/src/Development/Shake/ATS/Type.hs
--- a/src/Development/Shake/ATS/Type.hs
+++ b/src/Development/Shake/ATS/Type.hs
@@ -11,6 +11,7 @@
                                   , ATSToolConfig (..)
                                   , ATSGen (..)
                                   , HATSGen (..)
+                                  , Solver (..)
                                   -- * Lenses
                                   , atsTarget
                                   , hasPretty
@@ -31,6 +32,8 @@
                                   , linkTargets
                                   , cpphs
                                   , hsFile
+                                  , strip
+                                  , solver
                                   ) where
 
 import           Data.Binary         (Binary (..))
@@ -76,12 +79,19 @@
                   | SharedLibrary
                   deriving (Generic, Binary)
 
+data Solver = PatsSolve
+            | Z3
+            | Ignore
+            deriving (Generic, Binary)
+
 -- | Information about where to find @patscc@ and @patsopt@.
 data ATSToolConfig = ATSToolConfig { _patsHome     :: String -- ^ Value to be used for @PATSHOME@.
                                    , _patsHomeLocs :: String -- ^ Value to be used for @PATSHOMELOCS@.
                                    , _hasPretty    :: Bool -- ^ Whether to display errors via @pats-filter@
                                    , _cc           :: CCompiler -- ^ C compiler to be used
                                    , _linkStatic   :: Bool -- ^ Force static linking
+                                   , _solver       :: Solver
+                                   -- , _linkATSLib :: Bool -- ^ Whether to link against atslib
                                    } deriving (Generic, Binary)
 
 data HATSGen = HATSGen { satsFile :: FilePath -- ^ @.sats@ file containing type definitions
@@ -107,6 +117,7 @@
                            , _binTarget   :: FilePath -- ^ Target
                            , _otherDeps   :: [FilePath] -- ^ Other files to track.
                            , _tgtType     :: ArtifactType -- ^ Build type
+                           , _strip       :: Bool -- ^ Whether to strip generated artifacts
                            } deriving (Generic, Binary)
 
 -- | Data type containing information about Haskell components of a build. Any