From 39da2a42044973f9dd46ab3226eeed049d1a291b Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date: Wed, 22 Jan 2025 21:59:42 +0100
Subject: [PATCH] WIP conditional elaboration of theories for cvc5

---
 src/Language/Fixpoint/Smt/Interface.hs        |  20 +-
 src/Language/Fixpoint/Smt/Serialize.hs        |  21 +-
 src/Language/Fixpoint/Smt/Theories.hs         |  89 ++--
 src/Language/Fixpoint/Solver.hs               |   2 +-
 src/Language/Fixpoint/Solver/Common.hs        |   4 +-
 .../Fixpoint/Solver/Extensionality.hs         |  44 +-
 .../Fixpoint/Solver/GradualSolution.hs        |  27 +-
 src/Language/Fixpoint/Solver/Instantiate.hs   |   4 +-
 src/Language/Fixpoint/Solver/Interpreter.hs   |   2 +-
 src/Language/Fixpoint/Solver/PLE.hs           | 120 +++---
 src/Language/Fixpoint/Solver/Sanitize.hs      |  16 +-
 src/Language/Fixpoint/Solver/Solution.hs      | 123 +++---
 src/Language/Fixpoint/Solver/Solve.hs         |  43 +-
 src/Language/Fixpoint/SortCheck.hs            | 382 ++++++++++--------
 src/Language/Fixpoint/Types/Config.hs         |   8 +-
 src/Language/Fixpoint/Types/Environments.hs   |   8 +-
 src/Language/Fixpoint/Types/Graduals.hs       |  22 +-
 src/Language/Fixpoint/Types/Solutions.hs      |   7 +-
 src/Language/Fixpoint/Types/Sorts.hs          |  33 +-
 src/Language/Fixpoint/Types/Theories.hs       |  58 +--
 tests/test.hs                                 |   5 +
 21 files changed, 563 insertions(+), 475 deletions(-)

diff --git a/src/Language/Fixpoint/Smt/Interface.hs b/src/Language/Fixpoint/Smt/Interface.hs
index 6b27a06dc..8f8a8069e 100644
--- a/src/Language/Fixpoint/Smt/Interface.hs
+++ b/src/Language/Fixpoint/Smt/Interface.hs
@@ -156,7 +156,7 @@ checkValids cfg f xts ps
 {-# SCC command #-}
 command              :: Context -> Command -> IO Response
 --------------------------------------------------------------------------------
-command Ctx {..} !cmd       = do
+command Ctx{..} !cmd       = do
   -- whenLoud $ do LTIO.appendFile debugFile (s <> "\n")
   --               LTIO.putStrLn ("CMD-RAW:" <> s <> ":CMD-RAW:DONE")
   forM_ ctxLog $ \h -> do
@@ -173,7 +173,9 @@ command Ctx {..} !cmd       = do
             TE.decodeUtf8With (const $ const $ Just ' ') $
             LBS.toStrict resp
       parse respTxt
-    cmdBS = {-# SCC "Command-runSmt2" #-} runSmt2 ctxSymEnv cmd
+    cmdBS = {-# SCC "Command-runSmt2" #-}
+      {-let cmd' = tracepp "command" cmd in-}
+      runSmt2 ctxSymEnv cmd -- '
     parse resp      = do
       case A.parseOnly responseP resp of
         Left e  -> Misc.errorstar $ "SMTREAD:" ++ e
@@ -256,7 +258,7 @@ makeContextWithSEnv :: Config -> FilePath -> SymEnv -> IO Context
 makeContextWithSEnv cfg f env = do
   ctx     <- makeContext cfg f
   let ctx' = ctx {ctxSymEnv = env}
-  declare ctx'
+  declare (solver cfg) ctx'
   return ctx'
   -- where msg = "makeContextWithSEnv" ++ show env
 
@@ -400,7 +402,9 @@ smtCheckSat me p
    ans _   = False
 
 smtAssert :: Context -> Expr -> IO ()
-smtAssert me p  = interact' me (Assert Nothing p)
+smtAssert me p =
+  {- let p' = tracepp "smtAssert" p in -}
+  interact' me (Assert Nothing p {-p'-})
 
 smtDefineFunc :: Context -> Symbol -> [(Symbol, F.Sort)] -> F.Sort -> Expr -> IO ()
 smtDefineFunc me name symList rsort e =
@@ -462,9 +466,9 @@ z3_options
 
 
 --------------------------------------------------------------------------------
-declare :: Context -> IO ()
+declare :: SMTSolver -> Context -> IO ()
 --------------------------------------------------------------------------------
-declare me = do
+declare slv me = do
   forM_ dss    $           smtDataDecl me
   forM_ thyXTs $ uncurry $ smtDecl     me
   forM_ qryXTs $ uncurry $ smtDecl     me
@@ -481,7 +485,7 @@ declare me = do
     qryXTs     = fmap tx <$> filter (isKind 2) xts
     isKind n   = (n ==)  . symKind env . fst
     xts        = {- tracepp "symbolSorts" $ -} symbolSorts (F.seSort env)
-    tx         = elaborate    "declare" env
+    tx         = elaborate slv "declare" env
     ats        = funcSortVars env
 
 symbolSorts :: F.SEnv F.Sort -> [(F.Symbol, F.Sort)]
@@ -500,7 +504,7 @@ funcSortVars env  = [(var applyName  t       , appSort t) | t <- ts]
                  ++ [(var (lamArgSymbol i) t , argSort t) | t@(_,F.SInt) <- ts, i <- [1..Thy.maxLamArg] ]
   where
     var n         = F.symbolAtSmtName n env ()
-    ts            = M.keys (F.seAppls env)
+    ts            = {- tracepp "funcSortVars" $ -} M.keys (F.seAppls env)
     appSort (s,t) = ([F.SInt, s], t)
     lamSort (s,t) = ([s, t], F.SInt)
     argSort (s,_) = ([]    , s)
diff --git a/src/Language/Fixpoint/Smt/Serialize.hs b/src/Language/Fixpoint/Smt/Serialize.hs
index d14a2ead9..1b3c92fab 100644
--- a/src/Language/Fixpoint/Smt/Serialize.hs
+++ b/src/Language/Fixpoint/Smt/Serialize.hs
@@ -147,7 +147,7 @@ instance SMTLIB2 Expr where
   smt2 env (PAnd ps)        = parenSeqs ["and", smt2s env ps]
   smt2 _   (POr [])         = "false"
   smt2 env (POr ps)         = parenSeqs ["or", smt2s env ps]
-  smt2 env (PNot p)         = parenSeqs ["not", smt2  env p]
+  smt2 env (PNot p)         = parenSeqs ["not", smt2 env p]
   smt2 env (PImp p q)       = parenSeqs ["=>", smt2 env p, smt2 env q]
   smt2 env (PIff p q)       = parenSeqs ["=", smt2 env p, smt2 env q]
   smt2 env (PExist [] p)    = smt2 env p
@@ -155,7 +155,7 @@ instance SMTLIB2 Expr where
   smt2 env (PAll   [] p)    = smt2 env p
   smt2 env (PAll   xs p)    = parenSeqs ["forall", parens (smt2s env xs), smt2 env p]
   smt2 env (PAtom r e1 e2)  = mkRel env r e1 e2
-  smt2 env (ELam b e)       = smt2Lam   env b e
+  smt2 env (ELam b e)       = smt2Lam env b e
   smt2 env (ECoerc t1 t2 e) = smt2Coerc env t1 t2 e
   smt2 _   e                = panic ("smtlib2 Pred  " ++ show e)
 
@@ -176,7 +176,9 @@ smt2Var env x t
   | otherwise                   = smt2 env x
 
 smtLamArg :: SymEnv -> Symbol -> Sort -> Builder
-smtLamArg env x t = Builder.fromText $ symbolAtName x env () (FFunc t FInt)
+smtLamArg env x t =
+  {-let t' = tracepp "smtLamArg" t in-}
+  Builder.fromText $ symbolAtName x env () (FFunc t {-t'-} FInt)
 
 smt2VarAs :: SymEnv -> Symbol -> Sort -> Builder
 smt2VarAs env x t = parenSeqs ["as", smt2 env x, smt2SortMono x env t]
@@ -184,8 +186,10 @@ smt2VarAs env x t = parenSeqs ["as", smt2 env x, smt2SortMono x env t]
 smt2Lam :: SymEnv -> (Symbol, Sort) -> Expr -> Builder
 smt2Lam env (x, xT) full@(ECst _ eT) = parenSeqs [Builder.fromText lambda, x', smt2 env full]
   where
-    x'                          = smtLamArg env x xT
-    lambda                      = symbolAtName lambdaName env () (FFunc xT eT)
+    x'     = smtLamArg env x xT
+    lambda =
+      {- let eT' = tracepp "smt2Lam" eT in -}
+      symbolAtName lambdaName env () (FFunc xT eT {-eT'-})
 
 smt2Lam _ _ e
   = panic ("smtlib2: Cannot serialize unsorted lambda: " ++ showpp e)
@@ -193,7 +197,8 @@ smt2Lam _ _ e
 smt2App :: SymEnv -> Expr -> Builder
 smt2App env e@(EApp (EApp f e1) e2)
   | Just t <- unApplyAt f
-  = parenSeqs [Builder.fromText (symbolAtName applyName env e t), smt2s env [e1, e2]]
+  = {- let t' = tracepp "smt2App" t in -}
+    parenSeqs [Builder.fromText (symbolAtName applyName env e t {-t'-}), smt2s env [e1, e2]]
 smt2App env e
   | Just b <- Thy.smt2App smt2VarAs env f (smt2 env <$> es)
   = b
@@ -207,7 +212,9 @@ smt2Coerc env t1 t2 e
   | t1 == t2  = smt2 env e
   | otherwise = parenSeqs [Builder.fromText coerceFn , smt2 env e]
   where
-    coerceFn  = symbolAtName coerceName env (ECoerc t1 t2 e) t
+    coerceFn  =
+      {- let t' = tracepp "smt2Coerc" t in -}
+      symbolAtName coerceName env (ECoerc t1 t2 e) t {-t'-}
     t         = FFunc t1 t2
 
 splitEApp' :: Expr -> (Expr, [Expr])
diff --git a/src/Language/Fixpoint/Smt/Theories.hs b/src/Language/Fixpoint/Smt/Theories.hs
index 1717eba4a..d7725f597 100644
--- a/src/Language/Fixpoint/Smt/Theories.hs
+++ b/src/Language/Fixpoint/Smt/Theories.hs
@@ -133,7 +133,12 @@ bvSLeName  = "bvsle"
 bvSGtName  = "bvsgt"
 bvSGeName  = "bvsge"
 
-setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng :: (IsString a) => a -- Symbol
+mapDef, mapSel, mapSto :: (IsString a) => a
+mapDef   = "Map_default"
+mapSel   = "Map_select"
+mapSto   = "Map_store"
+
+setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng :: (IsString a) => a
 setEmpty = "Set_empty"
 setEmp   = "Set_emp"
 setCap   = "Set_cap"
@@ -145,11 +150,6 @@ setCup   = "Set_cup"
 setDif   = "Set_dif"
 setSng   = "Set_sng"
 
-mapDef, mapSel, mapSto :: (IsString a) => a
-mapDef   = "Map_default"
-mapSel   = "Map_select"
-mapSto   = "Map_store"
-
 bagEmpty, bagSng, bagCount, bagSub, bagCup, bagMax, bagMin :: (IsString a) => a
 bagEmpty = "Bag_empty"
 bagSng   = "Bag_sng"
@@ -165,7 +165,13 @@ bagMin   = "Bag_inter_min"
 -- taking either the greatest (bagMax) or the least (bagMin) of them.
 --   bagMax, bagMin : Map v Int -> Map v Int -> Map v Int
 
---- Array operations for sets
+--- Array operations for polymorphic maps
+arrConstM, arrStoreM, arrSelectM :: Symbol
+arrConstM  = "arr_const_m"
+arrStoreM  = "arr_store_m"
+arrSelectM = "arr_select_m"
+
+--- Array operations for sets (Z3)
 arrConstS, arrStoreS, arrSelectS, arrMapNotS, arrMapOrS, arrMapAndS, arrMapImpS :: Symbol
 arrConstS  = "arr_const_s"
 arrStoreS  = "arr_store_s"
@@ -176,13 +182,7 @@ arrMapOrS  = "arr_map_or"
 arrMapAndS = "arr_map_and"
 arrMapImpS = "arr_map_imp"
 
---- Array operations for polymorphic maps
-arrConstM, arrStoreM, arrSelectM :: Symbol
-arrConstM  = "arr_const_m"
-arrStoreM  = "arr_store_m"
-arrSelectM = "arr_select_m"
-
---- Array operations for bags
+--- Array operations for bags (Z3)
 arrConstB, arrStoreB, arrSelectB :: Symbol
 arrConstB  = "arr_const_b"
 arrStoreB  = "arr_store_b"
@@ -300,8 +300,8 @@ smt2SmtSort SInt         = "Int"
 smt2SmtSort SReal        = "Real"
 smt2SmtSort SBool        = "Bool"
 smt2SmtSort SString      = fromText string
---smt2SmtSort SSet         = fromText set
---smt2SmtSort SMap         = fromText map
+smt2SmtSort (SSet a)     = key "Set" (smt2SmtSort a)
+smt2SmtSort (SBag a)     = key "Bag" (smt2SmtSort a)
 smt2SmtSort (SArray a b) = key2 "Array" (smt2SmtSort a) (smt2SmtSort b)
 smt2SmtSort (SBitVec n)  = key "_ BitVec" (bShow n)
 smt2SmtSort (SVar n)     = "T" <> bShow n
@@ -321,6 +321,8 @@ smt2App _ env ex@(dropECst -> EVar f) [d]
   | f == arrConstS = Just (key (key "as const" (getTarget ex)) d)
   | f == arrConstB = Just (key (key "as const" (getTarget ex)) d)
   | f == arrConstM = Just (key (key "as const" (getTarget ex)) d)
+  | f == setEmpty  = Just (key "as set.empty" (getTarget ex))
+  | f == bagEmpty  = Just (key "as bag.empty" (getTarget ex))
   where
     getTarget :: Expr -> Builder
     -- const is a function, but SMT expects only the output sort
@@ -386,8 +388,15 @@ interpSymbols :: SMTSolver -> [(Symbol, TheorySymbol)]
 --------------------------------------------------------------------------------
 interpSymbols cfg =
   [
-  -- TODO we'll probably need two versions of these - one for sets and one for maps
-    interpSym arrConstS  "const"  (FAbs 0 $ FFunc boolSort setArrSort)
+    -- maps
+
+    interpSym arrConstM  "const"  (FAbs 0 $ FFunc (FVar 1) mapArrSort)
+  , interpSym arrSelectM "select" (FAbs 0 $ FFunc mapArrSort $ FFunc (FVar 0) (FVar 1))
+  , interpSym arrStoreM  "store"  (FAbs 0 $ FFunc mapArrSort $ FFunc (FVar 0) $ FFunc (FVar 1) mapArrSort)
+
+    -- Z3 sets (arrays of bools)
+
+  , interpSym arrConstS  "const"  (FAbs 0 $ FFunc boolSort setArrSort)
   , interpSym arrSelectS "select" (FAbs 0 $ FFunc setArrSort $ FFunc (FVar 0) boolSort)
   , interpSym arrStoreS  "store"  (FAbs 0 $ FFunc setArrSort $ FFunc (FVar 0) $ FFunc boolSort setArrSort)
 
@@ -396,9 +405,7 @@ interpSymbols cfg =
   , interpSym arrMapAndS "(_ map and)" (FFunc setArrSort $ FFunc setArrSort setArrSort)
   , interpSym arrMapImpS "(_ map =>)"  (FFunc setArrSort $ FFunc setArrSort setArrSort)
 
-  , interpSym arrConstM  "const"  (FAbs 0 $ FFunc (FVar 1) mapArrSort)
-  , interpSym arrSelectM "select" (FAbs 0 $ FFunc mapArrSort $ FFunc (FVar 0) (FVar 1))
-  , interpSym arrStoreM  "store"  (FAbs 0 $ FFunc mapArrSort $ FFunc (FVar 0) $ FFunc (FVar 1) mapArrSort)
+    -- Z3 bags (arrays of ints)
 
   , interpSym arrConstB  "const"  (FAbs 0 $ FFunc intSort bagArrSort)
   , interpSym arrSelectB "select" (FAbs 0 $ FFunc bagArrSort $ FFunc (FVar 0) intSort)
@@ -409,28 +416,32 @@ interpSymbols cfg =
   , interpSym arrMapGtB   "(_ map (> (Int Int) Bool))"       (FFunc bagArrSort $ FFunc bagArrSort setArrSort)
   , interpSym arrMapIteB  "(_ map (ite (Bool Int Int) Int))" (FFunc setArrSort $ FFunc bagArrSort $ FFunc bagArrSort bagArrSort)
 
-  , interpSym setEmp   setEmp   (FAbs 0 $ FFunc (setSort $ FVar 0) boolSort)
-  , interpSym setEmpty setEmpty (FAbs 0 $ FFunc intSort (setSort $ FVar 0))
-  , interpSym setSng   setSng   (FAbs 0 $ FFunc (FVar 0) (setSort $ FVar 0))
-  , interpSym setAdd   setAdd   setAddSort
-  , interpSym setCup   setCup   setBopSort
-  , interpSym setCap   setCap   setBopSort
-  , interpSym setMem   setMem   setMemSort
-  , interpSym setDif   setDif   setBopSort
-  , interpSym setSub   setSub   setCmpSort
-  , interpSym setCom   setCom   setCmpSort
-
   , interpSym mapDef   mapDef  mapDefSort
   , interpSym mapSel   mapSel  mapSelSort
   , interpSym mapSto   mapSto  mapStoSort
 
-  , interpSym bagEmpty bagEmpty (FAbs 0 $ FFunc intSort (bagSort $ FVar 0))
-  , interpSym bagSng   bagSng   (FAbs 0 $ FFunc (FVar 0) $ FFunc intSort (bagSort $ FVar 0))
-  , interpSym bagCount bagCount bagCountSort
-  , interpSym bagCup   bagCup   bagBopSort
-  , interpSym bagMax   bagMax   bagBopSort
-  , interpSym bagMin   bagMin   bagBopSort
-  , interpSym bagSub   bagSub   bagSubSort
+  -- CVC5 sets
+
+  , interpSym setEmp   "set.is_empty"   (FAbs 0 $ FFunc (setSort $ FVar 0) boolSort)
+  , interpSym setEmpty "set.empty"      (FAbs 0 $ FFunc intSort (setSort $ FVar 0))
+  , interpSym setSng   "set.singleton"  (FAbs 0 $ FFunc (FVar 0) (setSort $ FVar 0))
+  , interpSym setAdd   "set.insert"     setAddSort  -- TODO broken! the order is flipped
+  , interpSym setCup   "set.union"      setBopSort
+  , interpSym setCap   "set.inter"      setBopSort
+  , interpSym setMem   "set.member"     setMemSort
+  , interpSym setDif   "set.minus"      setBopSort
+  , interpSym setSub   "set.subset"     setCmpSort
+  , interpSym setCom   "set.complement" (FAbs 0 $ FFunc (setSort $ FVar 0) (setSort $ FVar 0))
+
+  -- CVC5 bags
+
+  , interpSym bagEmpty "bag.empty"          (FAbs 0 $ FFunc intSort (bagSort $ FVar 0))
+  , interpSym bagSng   "bag"                (FAbs 0 $ FFunc (FVar 0) $ FFunc intSort (bagSort $ FVar 0))
+  , interpSym bagCount "bag.count"          bagCountSort -- TODO broken! the order is flipped
+  , interpSym bagCup   "bag.union_disjoint" bagBopSort
+  , interpSym bagMax   "bag.union_max"      bagBopSort
+  , interpSym bagMin   "bag.inter_min"      bagBopSort
+  , interpSym bagSub   "bag.subbag"         bagSubSort
 
   -- , interpSym bvOrName  "bvor"  bvBopSort
   -- , interpSym bvAndName "bvand" bvBopSort
diff --git a/src/Language/Fixpoint/Solver.hs b/src/Language/Fixpoint/Solver.hs
index 3f58c71c9..59aadf24d 100644
--- a/src/Language/Fixpoint/Solver.hs
+++ b/src/Language/Fixpoint/Solver.hs
@@ -250,7 +250,7 @@ simplifyFInfo !cfg !fi0 = do
   -- writeLoud $ "fq file after defunc: \n" ++ render (toFixpoint cfg si4)
   -- putStrLn $ "AXIOMS: " ++ showpp (asserts si4)
   loudDump 2 cfg si4
-  let si5  = {- SCC "elaborate" -} elaborate (atLoc dummySpan "solver") (symbolEnv cfg si4) si4
+  let si5  = {- SCC "elaborate" -} elaborate (solver cfg) (atLoc dummySpan "solver") (symbolEnv cfg si4) si4
   -- writeLoud $ "fq file after elaborate: \n" ++ render (toFixpoint cfg si5)
   loudDump 3 cfg si5
   let si6 = if extensionality cfg then {- SCC "expand" -} expand cfg si5 else si5
diff --git a/src/Language/Fixpoint/Solver/Common.hs b/src/Language/Fixpoint/Solver/Common.hs
index f62dccea5..a9fe8fc99 100644
--- a/src/Language/Fixpoint/Solver/Common.hs
+++ b/src/Language/Fixpoint/Solver/Common.hs
@@ -2,7 +2,7 @@
 
 module Language.Fixpoint.Solver.Common (askSMT, toSMT) where
 
-import Language.Fixpoint.Types.Config (Config)
+import Language.Fixpoint.Types.Config (Config, solver)
 import Language.Fixpoint.Smt.Interface (Context(..), checkValidWithContext)
 import Language.Fixpoint.Types
 import Language.Fixpoint.Types.Visitor (kvarsExpr)
@@ -24,7 +24,7 @@ askSMT cfg ctx xs e
 toSMT :: String -> Config -> Context -> [(Symbol, Sort)] -> Expr -> Pred
 toSMT msg cfg ctx xs e =
     defuncAny cfg symenv .
-        elaborate (dummyLoc msg) (elabEnv xs) .
+        elaborate (solver cfg) (dummyLoc msg) (elabEnv xs) .
             mytracepp ("toSMT from " ++ msg ++ showpp e) $
                 e
   where
diff --git a/src/Language/Fixpoint/Solver/Extensionality.hs b/src/Language/Fixpoint/Solver/Extensionality.hs
index b827ffbbb..b3a61830b 100644
--- a/src/Language/Fixpoint/Solver/Extensionality.hs
+++ b/src/Language/Fixpoint/Solver/Extensionality.hs
@@ -26,40 +26,40 @@ mytracepp = notracepp
 expand :: Config -> SInfo a -> SInfo a
 expand cfg si = evalState (ext si) $ initST (symbolEnv cfg si) (ddecls si)
   where
-    ext ::SInfo a -> Ex a (SInfo a)
-    ext = extend
+    ext :: SInfo a -> Ex a (SInfo a)
+    ext a = extend a (solver cfg)
 
 
 class Extend ann a where
-  extend :: a -> Ex ann a
+  extend :: a -> SMTSolver -> Ex ann a
 
 
 instance Extend a (SInfo a) where
-  extend si = do
+  extend si slv = do
     setBEnv (bs si)
-    cm'      <- extend (cm si)
+    cm'      <- extend (cm si) slv
     bs'      <- gets exbenv
     return $ si{ cm = cm' , bs = bs' }
 
 instance (Extend ann a) => Extend ann (M.HashMap SubcId a) where
-  extend h = M.fromList <$> mapM extend (M.toList h)
+  extend h slv  = M.fromList <$> mapM (`extend` slv) (M.toList h)
 
 instance (Extend ann a, Extend ann b) => Extend ann (a,b) where
-  extend (a,b) = (,) <$> extend a <*> extend b
+  extend (a,b) slv = (,) <$> extend a slv <*> extend b slv
 
 instance Extend ann SubcId where
-  extend i = return i
+  extend i _ = return i
 
 instance Extend a (SimpC a) where
-  extend c = do
+  extend c slv = do
     setExBinds (_cenv c)
-    rhs <- extendExpr (sinfo c) Pos (_crhs c)
+    rhs <- extendExpr (sinfo c) slv Pos (_crhs c)
     is  <- gets exbinds
     return $ c{_crhs = rhs, _cenv = is }
 
 
-extendExpr :: a -> Pos -> Expr -> Ex a Expr
-extendExpr ann p expr'
+extendExpr :: a -> SMTSolver -> Pos -> Expr -> Ex a Expr
+extendExpr ann slv p expr'
   | p == Pos
   = mapMPosExpr Pos goP e' >>= mapMPosExpr Pos goN
   | otherwise
@@ -69,12 +69,12 @@ extendExpr ann p expr'
       goP Pos (PAtom b e1 e2)
        | b == Eq || b == Ne
        , Just s <- getArg (exprSort "extensionality" e1)
-       = mytracepp ("extending POS = " ++ showpp expr') <$> (extendRHS ann b e1 e2 s >>= goP Pos)
+       = mytracepp ("extending POS = " ++ showpp expr') <$> (extendRHS ann slv b e1 e2 s >>= goP Pos)
       goP _ e = return e
       goN Neg (PAtom b e1 e2)
        | b == Eq || b == Ne
        , Just s <- getArg (exprSort "extensionality" e1)
-       = mytracepp ("extending NEG = " ++ showpp expr') <$> (extendLHS ann b e1 e2 s >>= goN Neg)
+       = mytracepp ("extending NEG = " ++ showpp expr') <$> (extendLHS ann slv b e1 e2 s >>= goN Neg)
       goN _ e = return e
 
 getArg :: Sort -> Maybe Sort
@@ -82,16 +82,16 @@ getArg s = case bkFFunc s of
              Just (_, a:_:_) -> Just a
              _                -> Nothing
 
-extendRHS, extendLHS :: a -> Brel -> Expr -> Expr -> Sort -> Ex a Expr
-extendRHS ann b e1 e2 s =
+extendRHS, extendLHS :: a -> SMTSolver -> Brel -> Expr -> Expr -> Sort -> Ex a Expr
+extendRHS ann slv b e1 e2 s =
   do es <- generateArguments ann s
-     mytracepp "extendRHS = " . pAnd <$> mapM (makeEq b e1 e2) es
+     mytracepp "extendRHS = " . pAnd <$> mapM (makeEq slv b e1 e2) es
 
-extendLHS ann b e1 e2 s =
+extendLHS ann slv b e1 e2 s =
   do es  <- generateArguments ann s
      dds <- gets exddecl
      is  <- instantiate ann dds s
-     mytracepp "extendLHS = " . pAnd . (PAtom b e1 e2:) <$> mapM (makeEq b e1 e2) (es ++ is)
+     mytracepp "extendLHS = " . pAnd . (PAtom b e1 e2:) <$> mapM (makeEq slv b e1 e2) (es ++ is)
 
 generateArguments :: a -> Sort -> Ex a [Expr]
 generateArguments ann srt = do
@@ -100,10 +100,10 @@ generateArguments ann srt = do
     Left dds -> mapM (freshArgDD ann) dds
     Right s  -> (\x -> [EVar x]) <$> freshArgOne ann s
 
-makeEq :: Brel-> Expr -> Expr -> Expr -> Ex ann Expr
-makeEq b e1 e2 e = do
+makeEq :: SMTSolver -> Brel -> Expr -> Expr -> Expr -> Ex ann Expr
+makeEq slv b e1 e2 e = do
   env <- gets exenv
-  let elab = elaborate (dummyLoc "extensionality") env
+  let elab = elaborate slv (dummyLoc "extensionality") env
   return $ PAtom b (elab $ EApp (unElab e1) e)  (elab $ EApp (unElab e2) e)
 
 instantiate :: a -> [DataDecl]  -> Sort -> Ex a [Expr]
diff --git a/src/Language/Fixpoint/Solver/GradualSolution.hs b/src/Language/Fixpoint/Solver/GradualSolution.hs
index 2c060cb2d..292bbfa10 100644
--- a/src/Language/Fixpoint/Solver/GradualSolution.hs
+++ b/src/Language/Fixpoint/Solver/GradualSolution.hs
@@ -26,7 +26,7 @@ import Language.Fixpoint.SortCheck
 --------------------------------------------------------------------------------
 init :: (F.Fixpoint a) => Config -> F.SInfo a -> [(F.KVar, (F.GWInfo, [F.Expr]))]
 --------------------------------------------------------------------------------
-init cfg si = map (elab . refineG si qs genv) gs `using` parList rdeepseq
+init cfg si = map (elab . refineG slv si qs genv) gs `using` parList rdeepseq
   where
     qs         = F.quals si
     gs         = snd <$> gs0
@@ -34,20 +34,21 @@ init cfg si = map (elab . refineG si qs genv) gs `using` parList rdeepseq
 
     gs0        = L.filter (Cons.isGWfc . snd) $ M.toList (F.ws si)
 
-    elab (k, (x,es)) = (k, (x, elaborate (F.atLoc F.dummySpan "init") (sEnv (Cons.gsym x) (Cons.gsort x)) <$> es))
+    elab (k, (x,es)) = (k, (x, elaborate slv (F.atLoc F.dummySpan "init") (sEnv (Cons.gsym x) (Cons.gsort x)) <$> es))
 
     sEnv x s    = isEnv {F.seSort = F.insertSEnv x s (F.seSort isEnv)}
     isEnv       = symbolEnv cfg si
+    slv         = solver cfg
 
 
 --------------------------------------------------------------------------------
-refineG :: F.SInfo a -> [F.Qualifier] -> F.SEnv F.Sort -> F.WfC a -> (F.KVar, (F.GWInfo, [F.Expr]))
-refineG fi qs genv w = (k, (F.gwInfo w, Sol.qbExprs qb))
+refineG :: SMTSolver -> F.SInfo a -> [F.Qualifier] -> F.SEnv F.Sort -> F.WfC a -> (F.KVar, (F.GWInfo, [F.Expr]))
+refineG slv fi qs genv w = (k, (F.gwInfo w, Sol.qbExprs qb))
   where
-    (k, qb) = refine fi qs genv w
+    (k, qb) = refine slv fi qs genv w
 
-refine :: F.SInfo a -> [F.Qualifier] -> F.SEnv F.Sort -> F.WfC a -> (F.KVar, Sol.QBind)
-refine fi qs genv w = refineK (Cons.allowHOquals fi) env qs $ F.wrft w
+refine :: SMTSolver -> F.SInfo a -> [F.Qualifier] -> F.SEnv F.Sort -> F.WfC a -> (F.KVar, Sol.QBind)
+refine slv fi qs genv w = refineK slv (Cons.allowHOquals fi) env qs $ F.wrft w
   where
     env             = wenv <> genv
     wenv            = F.sr_sort <$> F.fromListSEnv (F.envCs (F.bs fi) (F.wenv w))
@@ -58,11 +59,11 @@ instConstants = F.fromListSEnv . filter notLit . F.toListSEnv . F.gLits
     notLit    = not . F.isLitSymbol . fst
 
 
-refineK :: Bool -> F.SEnv F.Sort -> [F.Qualifier] -> (F.Symbol, F.Sort, F.KVar) -> (F.KVar, Sol.QBind)
-refineK ho env qs (v, t, k) = (k, eqs')
+refineK :: SMTSolver -> Bool -> F.SEnv F.Sort -> [F.Qualifier] -> (F.Symbol, F.Sort, F.KVar) -> (F.KVar, Sol.QBind)
+refineK slv ho env qs (v, t, k) = (k, eqs')
    where
     eqs                     = instK ho env v t qs
-    eqs'                    = Sol.qbFilter (okInst env v t) eqs
+    eqs'                    = Sol.qbFilter (okInst slv env v t) eqs
 
 --------------------------------------------------------------------------------
 instK :: Bool
@@ -118,12 +119,12 @@ candidates env tyss tx =
     mono = So.isMono tx
 
 --------------------------------------------------------------------------------
-okInst :: F.SEnv F.Sort -> F.Symbol -> F.Sort -> Sol.EQual -> Bool
+okInst :: SMTSolver -> F.SEnv F.Sort -> F.Symbol -> F.Sort -> Sol.EQual -> Bool
 --------------------------------------------------------------------------------
-okInst env v t eq = isNothing tc
+okInst slv env v t eq = isNothing tc
   where
     sr            = F.RR t (F.Reft (v, p))
     p             = Sol.eqPred eq
-    tc            = So.checkSorted F.dummySpan env sr
+    tc            = So.checkSorted slv F.dummySpan env sr
 
 
diff --git a/src/Language/Fixpoint/Solver/Instantiate.hs b/src/Language/Fixpoint/Solver/Instantiate.hs
index 29f50caee..3b2b0277b 100644
--- a/src/Language/Fixpoint/Solver/Instantiate.hs
+++ b/src/Language/Fixpoint/Solver/Instantiate.hs
@@ -181,7 +181,7 @@ resSInfo :: Config -> SymEnv -> SInfo a -> InstRes -> SInfo a
 resSInfo cfg env info res = strengthenBinds info res'
   where
     res'     = M.fromList $ mytracepp  "ELAB-INST:  " $ zip is ps''
-    ps''     = zipWith (\i -> elaborate (atLoc dummySpan ("PLE1 " ++ show i)) env) is ps'
+    ps''     = zipWith (\i -> elaborate (solver cfg) (atLoc dummySpan ("PLE1 " ++ show i)) env) is ps'
     ps'      = defuncAny cfg env ps
     (is, ps) = unzip (M.toList res)
 
@@ -311,7 +311,7 @@ sInfo cfg env info ips = strengthenHyp info (mytracepp  "ELAB-INST:  " $ zip (fs
   where
     (is, ps)         = unzip ips
     ps'              = defuncAny cfg env ps
-    ps''             = zipWith (\(i, sp) -> elaborate (atLoc sp ("PLE1 " ++ show i)) env) is ps'
+    ps''             = zipWith (\(i, sp) -> elaborate (solver cfg) (atLoc sp ("PLE1 " ++ show i)) env) is ps'
 
 instSimpC :: Config -> SMT.Context -> BindEnv a -> AxiomEnv -> SubcId -> SimpC a -> IO Expr
 instSimpC cfg ctx bds aenv subId sub
diff --git a/src/Language/Fixpoint/Solver/Interpreter.hs b/src/Language/Fixpoint/Solver/Interpreter.hs
index b1ffdbb0c..f523bf19c 100644
--- a/src/Language/Fixpoint/Solver/Interpreter.hs
+++ b/src/Language/Fixpoint/Solver/Interpreter.hs
@@ -182,7 +182,7 @@ resSInfo :: Config -> SymEnv -> SInfo a -> InstRes -> SInfo a
 resSInfo cfg env info res = strengthenBinds info res'
   where
     res'     = M.fromList $ zip is ps''
-    ps''     = zipWith (\i -> elaborate (atLoc dummySpan ("PLE1 " ++ show i)) env) is ps'
+    ps''     = zipWith (\i -> elaborate (solver cfg) (atLoc dummySpan ("PLE1 " ++ show i)) env) is ps'
     ps'      = defuncAny cfg env ps
     (is, ps) = unzip (M.toList res)
 
diff --git a/src/Language/Fixpoint/Solver/PLE.hs b/src/Language/Fixpoint/Solver/PLE.hs
index fd29894aa..0b78da381 100644
--- a/src/Language/Fixpoint/Solver/PLE.hs
+++ b/src/Language/Fixpoint/Solver/PLE.hs
@@ -114,7 +114,7 @@ savePLEEqualities cfg info sEnv res = when (save cfg) $ do
             map (toFix . unElab) $ Set.toList $ Set.fromList $
             -- call elabExpr to try to bring equations that are missing
             -- some casts into a fully annotated form for comparison
-            map (elabExpr "savePLEEqualities" sEnv) $
+            map (elabExpr (solver cfg) "savePLEEqualities" sEnv) $
             concatMap conjuncts eqs
            )
       $+$ ""
@@ -156,7 +156,7 @@ instEnv cfg info cs restSolver ctx = do
     return $ InstEnv
        { ieCfg = cfg
        , ieSMT = ctx
-       , ieBEnv = coerceBindEnv $ bs info
+       , ieBEnv = coerceBindEnv (FC.solver cfg) (bs info)
        , ieAenv = ae info
        , ieCstrs = cs
        , ieKnowl = knowledge cfg ctx info
@@ -323,7 +323,7 @@ evalCandsLoop cfg ictx0 ctx γ = go ictx0 0
         else do liftIO $ SMT.smtAssert ctx (pAndNoDedup (S.toList $ icAssms ictx))
                 let ictx' = ictx { icAssms = mempty }
                     cands = S.toList $ icCands ictx
-                candss <- mapM (evalOne γ ictx' i) cands
+                candss <- mapM (evalOne (solver cfg) γ ictx' i) cands
                 us <- gets evNewEqualities
                 modify $ \st -> st { evNewEqualities = mempty }
                 let noCandidateChanged = and (zipWith eqCand candss cands)
@@ -349,7 +349,7 @@ resSInfo :: Config -> SymEnv -> SInfo a -> InstRes -> SInfo a
 resSInfo cfg env info res = strengthenBinds info res'
   where
     res'     = M.fromList $ zip is ps''
-    ps''     = zipWith (\i -> elaborate (atLoc dummySpan ("PLE1 " ++ show i)) env) is ps'
+    ps''     = zipWith (\i -> elaborate (solver cfg) (atLoc dummySpan ("PLE1 " ++ show i)) env) is ps'
     ps'      = defuncAny cfg env ps
     (is, ps) = unzip (M.toList res)
 
@@ -518,20 +518,20 @@ getAutoRws γ mSubcId =
 -- definitions. When REST is in effect, more than one expression might
 -- be returned because expressions can then be rewritten in more than one
 -- way.
-evalOne :: Knowledge -> ICtx -> Int -> Expr -> EvalST [Expr]
-evalOne γ ctx i e
-  | i > 0 || null (getAutoRws γ (icSubcId ctx)) = (:[]) . fst <$> eval γ ctx NoRW e
-evalOne γ ctx _ e | isExprRewritable e = do
+evalOne :: SMTSolver -> Knowledge -> ICtx -> Int -> Expr -> EvalST [Expr]
+evalOne slv γ ctx i e
+  | i > 0 || null (getAutoRws γ (icSubcId ctx)) = (:[]) . fst <$> eval slv γ ctx NoRW e
+evalOne slv γ ctx _ e | isExprRewritable e = do
     env <- get
     let oc :: OCAlgebra OCType RuntimeTerm IO
         oc = evOCAlgebra env
         rp = RP (contramap Rewrite.convert oc) [(e, PLE)] constraints
         constraints = OC.top oc
         emptyET = ExploredTerms.empty (EF (OC.union oc) (OC.notStrongerThan oc) (OC.refine oc)) ExploreWhenNeeded
-    es <- evalREST γ ctx rp
+    es <- evalREST slv γ ctx rp
     modify $ \st -> st { explored = Just emptyET }
     return es
-evalOne _ _ _ _ = return []
+evalOne _ _ _ _ _ = return []
 
 -- The FuncNormal and RWNormal evaluation strategies are used for REST
 -- For example, consider the following function:
@@ -589,11 +589,11 @@ feSeq xs = (map fst xs, feAny (map snd xs))
 --
 -- Also adds to the monad state all the unfolding equalities that have been
 -- discovered as necessary.
-eval :: Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
-eval γ ctx et = go
+eval :: SMTSolver -> Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
+eval slv γ ctx et = go
   where
-    go (ELam (x,s) e)   = evalELam γ ctx et (x, s) e
-    go e@EIte{}         = evalIte γ ctx et e
+    go (ELam (x,s) e)   = evalELam slv γ ctx et (x, s) e
+    go e@EIte{}         = evalIte slv γ ctx et e
     go (ECoerc s t e)   = mapFE (ECoerc s t)  <$> go e
     go e@(EApp _ _)     =
       case splitEAppThroughECst e of
@@ -601,23 +601,23 @@ eval γ ctx et = go
           -- Just evaluate the arguments first, to give rewriting a chance to step in
           -- if necessary
           do
-            (es', finalExpand) <- feSeq <$> mapM (eval γ ctx et) es
+            (es', finalExpand) <- feSeq <$> mapM (eval slv γ ctx et) es
             if es /= es'
               then return (eApps f es', finalExpand)
               else do
                 (f', fe) <- case dropECst f of
                   EVar _ -> pure (f, noExpand)
                   _      -> go f
-                (me', fe') <- evalApp γ ctx f' es et
+                (me', fe') <- evalApp slv γ ctx f' es et
                 return (Mb.fromMaybe (eApps f' es') me', fe <|> fe')
        (f, es) ->
           do
             (f', fe1) <- case dropECst f of
               EVar _ -> pure (f, noExpand)
               _      -> go f
-            (es', fe2) <- feSeq <$> mapM (eval γ ctx et) es
+            (es', fe2) <- feSeq <$> mapM (eval slv γ ctx et) es
             let fe = fe1 <|> fe2
-            (me', fe') <- evalApp γ ctx f' es' et
+            (me', fe') <- evalApp slv γ ctx f' es' et
             return (Mb.fromMaybe (eApps f' es') me', fe <|> fe')
 
     go (PAtom r e1 e2) = binOp (PAtom r) e1 e2
@@ -634,7 +634,7 @@ eval γ ctx et = go
     go (PAnd es)        = efAll PAnd (go `traverse` es)
     go (POr es)         = efAll POr (go `traverse` es)
     go e | EVar _ <- dropECst e = do
-      (me', fe) <- evalApp γ ctx e [] et
+      (me', fe) <- evalApp slv γ ctx e [] et
       return (Mb.fromMaybe e me', fe)
     go (ECst e t)       = do (e', fe) <- go e
                              return (ECst e' t, fe)
@@ -652,8 +652,8 @@ eval γ ctx et = go
 
 -- | 'evalELamb' produces equations that preserve the context of a rewrite
 -- so equations include any necessary lambda bindings.
-evalELam :: Knowledge -> ICtx -> EvalType -> (Symbol, Sort) -> Expr -> EvalST (Expr, FinalExpand)
-evalELam γ ctx et (x, s) e
+evalELam :: SMTSolver -> Knowledge -> ICtx -> EvalType -> (Symbol, Sort) -> Expr -> EvalST (Expr, FinalExpand)
+evalELam slv γ ctx et (x, s) e
   | not $ isEtaSymbol x = do
     -- We need to refresh it as for some reason names bound by lambdas
     -- present in the source code are getting declared twice.
@@ -663,17 +663,17 @@ evalELam γ ctx et (x, s) e
     let newBody = subst (mkSubst [(x, EVar xFresh)]) e
 
     modify $ \st -> st
-      { evNewEqualities 
+      { evNewEqualities
         = S.insert (ELam (x, s) e, ELam (xFresh, s) newBody)
-                   (evNewEqualities st) 
+                   (evNewEqualities st)
       }
 
-    evalELam γ ctx et (xFresh, s) newBody
-  where 
+    evalELam slv γ ctx et (xFresh, s) newBody
+  where
     isEtaSymbol :: Symbol -> Bool
     isEtaSymbol = isPrefixOfSym "eta"
 
-evalELam γ ctx et (x, s) e = do
+evalELam slv γ ctx et (x, s) e = do
     oldPendingUnfoldings <- gets evPendingUnfoldings
     oldEqs <- gets evNewEqualities
 
@@ -681,7 +681,7 @@ evalELam γ ctx et (x, s) e = do
     modify $ \st -> st
       { evEnv = insertSymEnv x s $ evEnv st }
 
-    (e', fe) <- eval (γ { knLams = (x, s) : knLams γ }) ctx et e
+    (e', fe) <- eval slv (γ { knLams = (x, s) : knLams γ }) ctx et e
     let e2' = simplify γ ctx e'
         elam = ELam (x, s) e
     -- Discard the old equalities which miss the lambda binding
@@ -767,15 +767,15 @@ deANF binds = map $ inlineInExpr (`HashMap.Lazy.lookup` bindEnv)
 -- The main difference with 'eval' is that 'evalREST' takes into account
 -- autorewrites.
 --
-evalREST :: Knowledge -> ICtx -> RESTParams OCType -> EvalST [Expr]
-evalREST γ ctx rp = do
+evalREST :: SMTSolver -> Knowledge -> ICtx -> RESTParams OCType -> EvalST [Expr]
+evalREST slv γ ctx rp = do
   env <- get
   cacheRef <- liftIO $ newIORef $ evSMTCache env
-  evalRESTWithCache cacheRef γ ctx [] rp
+  evalRESTWithCache cacheRef slv γ ctx [] rp
 
 evalRESTWithCache
-  :: IORef (M.HashMap Expr Bool) -> Knowledge -> ICtx -> [Expr] -> RESTParams OCType -> EvalST [Expr]
-evalRESTWithCache cacheRef _ ctx acc rp
+  :: IORef (M.HashMap Expr Bool) -> SMTSolver -> Knowledge -> ICtx -> [Expr] -> RESTParams OCType -> EvalST [Expr]
+evalRESTWithCache cacheRef _ _ ctx acc rp
   | pathExprs <- map fst (mytracepp "EVAL1: path" $ path rp)
   , e         <- last pathExprs
   , Just v    <- M.lookup e (icSimpl ctx)
@@ -787,7 +787,7 @@ evalRESTWithCache cacheRef _ ctx acc rp
       })
     return (v : acc)
 
-evalRESTWithCache cacheRef γ ctx acc rp =
+evalRESTWithCache cacheRef slv γ ctx acc rp =
   do
     mexploredTerms <- gets explored
     case mexploredTerms of
@@ -802,10 +802,10 @@ evalRESTWithCache cacheRef γ ctx acc rp =
 
           -- liftIO $ putStrLn $ (show $ length possibleRWs) ++ " rewrites allowed at path length " ++ (show $ (map snd $ path rp))
           (e', FE fe) <- do
-            r@(ec, _) <- eval γ ctx FuncNormal exprs
+            r@(ec, _) <- eval slv γ ctx FuncNormal exprs
             if ec /= exprs
               then return r
-              else eval γ ctx RWNormal exprs
+              else eval slv γ ctx RWNormal exprs
 
           let evalIsNewExpr = e' `L.notElem` pathExprs
           let exprsToAdd    = [e' | evalIsNewExpr]  ++ map (\(_, e, _) -> e) rws
@@ -830,11 +830,11 @@ evalRESTWithCache cacheRef γ ctx acc rp =
 
           acc'' <- if evalIsNewExpr
             then if fe && any isRW (path rp)
-              then (:[]) . fst <$> eval γ (addConst (exprs, e')) NoRW e'
-              else evalRESTWithCache cacheRef γ (addConst (exprs, e')) acc' (rpEval newEqualities e')
+              then (:[]) . fst <$> eval slv γ (addConst (exprs, e')) NoRW e'
+              else evalRESTWithCache cacheRef slv γ (addConst (exprs, e')) acc' (rpEval newEqualities e')
             else return acc'
 
-          foldM (\r rw -> evalRESTWithCache cacheRef γ ctx r (rpRW rw)) acc'' rws
+          foldM (\r rw -> evalRESTWithCache cacheRef slv γ ctx r (rpRW rw)) acc'' rws
         else
           return acc
   where
@@ -941,8 +941,8 @@ evalRESTWithCache cacheRef γ ctx acc rp =
 
 -- | @evalApp kn ctx e es@ unfolds expressions in @eApps e es@ using rewrites
 -- and equations
-evalApp :: Knowledge -> ICtx -> Expr -> [Expr] -> EvalType -> EvalST (Maybe Expr, FinalExpand)
-evalApp γ ctx e0 es et
+evalApp :: SMTSolver -> Knowledge -> ICtx -> Expr -> [Expr] -> EvalType -> EvalST (Maybe Expr, FinalExpand)
+evalApp slv γ ctx e0 es et
   | EVar f <- dropECst e0
   , Just eq <- Map.lookup f (knAms γ)
   , length (eqArgs eq) <= length es
@@ -954,10 +954,10 @@ evalApp γ ctx e0 es et
          -- See Note [Elaboration for eta expansion].
          let newE = substEq env eq es1
          newE' <- if icEtaBetaFlag ctx
-                    then elaborateExpr "EvalApp unfold full: " newE
+                    then elaborateExpr slv "EvalApp unfold full: " newE
                     else pure newE
 
-         (e', fe) <- evalIte γ ctx et newE'        -- TODO:FUEL this is where an "unfolding" happens, CHECK/BUMP counter
+         (e', fe) <- evalIte slv γ ctx et newE'        -- TODO:FUEL this is where an "unfolding" happens, CHECK/BUMP counter
          let e2' = stripPLEUnfold e'
          let e3' = simplify γ ctx (eApps e2' es2)  -- reduces a bit the equations
 
@@ -997,7 +997,7 @@ evalApp γ ctx e0 es et
     guardOf (EIte g _ _) = Just g
     guardOf _ = Nothing
 
-evalApp γ ctx e0 args@(e:es) _
+evalApp _ γ ctx e0 args@(e:es) _
   | EVar f <- dropECst e0
   , (d, as) <- splitEAppThroughECst e
   , EVar dc <- dropECst d
@@ -1013,7 +1013,7 @@ evalApp γ ctx e0 args@(e:es) _
         { evNewEqualities = S.insert (eApps e0 args, simplify γ ctx newE) (evNewEqualities st) }
     return (Just newE, noExpand)
 
-evalApp γ ctx e0 es _et
+evalApp _ γ ctx e0 es _et
   | eqs@(_:_) <- noUserDataMeasureEqs γ (eApps e0 es)
   = do
        let eqs' = map (second $ simplify γ ctx) eqs
@@ -1021,7 +1021,7 @@ evalApp γ ctx e0 es _et
          st { evNewEqualities = foldr S.insert (evNewEqualities st) eqs' }
        return (Nothing, noExpand)
 
-evalApp γ ctx e0 es et
+evalApp slv γ ctx e0 es et
   | ELam (argName, _) body <- dropECst e0
   , lambdaArg:remArgs <- es
   , icEtaBetaFlag ctx || icExtensionalityFlag ctx
@@ -1032,7 +1032,7 @@ evalApp γ ctx e0 es et
           useFuel argName
           let argSubst = mkSubst [(argName, lambdaArg)]
           let body' = subst argSubst body
-          (body'', fe) <- evalIte γ ctx et body'
+          (body'', fe) <- evalIte slv γ ctx et body'
           let simpBody = simplify γ ctx (eApps body'' remArgs)
           modify $ \st ->
             st { evNewEqualities = S.insert (eApps e0 es, simpBody) (evNewEqualities st) }
@@ -1040,7 +1040,7 @@ evalApp γ ctx e0 es et
         else do
           return (Nothing, noExpand)
 
-evalApp _ ctx e0 es _
+evalApp _ _ ctx e0 es _
   | icLocalRewritesFlag ctx
   , EVar f <- dropECst e0
   , Just rw <- lookupRewrite f $ icLRWs ctx
@@ -1051,7 +1051,7 @@ evalApp _ ctx e0 es _
         { evNewEqualities = S.insert (eApps e0 es, expandedTerm) (evNewEqualities st) }
       return (Just expandedTerm, expand)
 
-evalApp _γ ctx e0 es _et
+evalApp _ _γ ctx e0 es _et
   -- We check the annotation instead of the equations in γ for two reasons.
   --
   -- First, we want to eta expand functions that might not be reflected. Suppose
@@ -1093,23 +1093,23 @@ evalApp _γ ctx e0 es _et
 
     mkLams subject binds = foldr ELam subject binds
 
-evalApp _ _ctx _e0 _es _ = do
+evalApp _ _ _ctx _e0 _es _ = do
   return (Nothing, noExpand)
 
 -- | Evaluates if-then-else statements until they can't be evaluated anymore
 -- or some other expression is found.
-evalIte :: Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
-evalIte γ ctx et (ECst e t) = do
-  (e', fe) <- evalIte γ ctx et e
+evalIte :: SMTSolver -> Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
+evalIte slv γ ctx et (ECst e t) = do
+  (e', fe) <- evalIte slv γ ctx et e
   return (ECst e' t, fe)
-evalIte γ ctx et (EIte i e1 e2) = do
-      (b, _) <- eval γ ctx et i
+evalIte slv γ ctx et (EIte i e1 e2) = do
+      (b, _) <- eval slv γ ctx et i
       b'  <- mytracepp ("evalEIt POS " ++ showpp (i, b)) <$> isValidCached γ b
       case b' of
-        Just True -> evalIte γ ctx et e1
-        Just False -> evalIte γ ctx et e2
+        Just True -> evalIte slv γ ctx et e1
+        Just False -> evalIte slv γ ctx et e2
         _ -> return (EIte b e1 e2, expand)
-evalIte _ _ _ e' = return (e', noExpand)
+evalIte _ _ _ _ e' = return (e', noExpand)
 
 -- | Creates equations that explain how to rewrite a given constructor
 -- application with all measures that aren't user data measures
@@ -1458,11 +1458,11 @@ makeFreshEtaNames n = replicateM n makeFreshName
       modify $ \st -> st { freshEtaNames = 1 + freshEtaNames st }
       pure $ etaExpSymbol ident
 
-elaborateExpr :: String -> Expr -> EvalST Expr
-elaborateExpr msg e = do
+elaborateExpr :: SMTSolver -> String -> Expr -> EvalST Expr
+elaborateExpr slv msg e = do
   let elabSpan = atLoc dummySpan msg
   symEnv' <- gets evEnv
-  pure $ unApply $ elaborate elabSpan symEnv' e
+  pure $ unApply $ elaborate slv elabSpan symEnv' e
 
 -- | Returns False if there is a fuel count in the evaluation environment and
 -- the fuel count exceeds the maximum. Returns True otherwise.
diff --git a/src/Language/Fixpoint/Solver/Sanitize.hs b/src/Language/Fixpoint/Solver/Sanitize.hs
index 15ac71063..4ffa5b925 100644
--- a/src/Language/Fixpoint/Solver/Sanitize.hs
+++ b/src/Language/Fixpoint/Solver/Sanitize.hs
@@ -36,6 +36,8 @@ import           Data.Maybe          (isNothing, mapMaybe, fromMaybe)
 import           Control.Monad       ((>=>))
 import           Text.PrettyPrint.HughesPJ
 
+-- import Debug.Trace
+
 type SanitizeM a = Either E.Error a
 
 --------------------------------------------------------------------------------
@@ -399,15 +401,17 @@ badRhs1 (i, c) = E.err E.dummySpan $ vcat [ "Malformed RHS for constraint id" <+
 --   it makes it hard to actually find the fundefs within (breaking PLE.)
 --------------------------------------------------------------------------------
 symbolEnv :: Config -> F.SInfo a -> F.SymEnv
-symbolEnv cfg si = F.symEnv sEnv tEnv ds lits (ts ++ ts')
+symbolEnv cfg si = F.symEnv sEnv' tEnv ds lits (ts ++ ts')
   where
     ts'          = applySorts ae'
-    ae'          = elaborate (F.atLoc E.dummySpan "symbolEnv") env0 (F.ae si)
-    env0         = F.symEnv sEnv tEnv ds lits ts
-    tEnv         = Thy.theorySymbols (Cfg.solver cfg) ds
+    ae'          = elaborate slv (F.atLoc E.dummySpan "symbolEnv") env0 (F.ae si)
+    env0         = F.symEnv sEnv' tEnv ds lits ts
+    tEnv         = Thy.theorySymbols slv ds
     ds           = F.ddecls si
-    ts           = Misc.setNub (applySorts si ++ [t | (_, t) <- F.toListSEnv sEnv])
-    sEnv         = F.coerceSortEnv $ (F.tsSort <$> tEnv) `mappend` F.fromListSEnv xts
+    ts           = Misc.setNub (applySorts si ++ [t | (_, t) <- F.toListSEnv sEnv'])
+    sEnv'        = F.coerceSortEnv slv sEnv
+    slv          = Cfg.solver cfg
+    sEnv         = (F.tsSort <$> tEnv) `mappend` F.fromListSEnv xts
     xts          = symbolSorts cfg si ++ alits
     lits         = F.dLits si `F.unionSEnv'` F.fromListSEnv alits
     alits        = litsAEnv $ F.ae si
diff --git a/src/Language/Fixpoint/Solver/Solution.hs b/src/Language/Fixpoint/Solver/Solution.hs
index a75adbc8a..0fabfb14c 100644
--- a/src/Language/Fixpoint/Solver/Solution.hs
+++ b/src/Language/Fixpoint/Solver/Solution.hs
@@ -48,7 +48,7 @@ init :: (F.Fixpoint a) => Config -> F.SInfo a -> S.HashSet F.KVar -> Sol.Solutio
 --------------------------------------------------------------------------------
 init cfg si ks_ = Sol.fromList symEnv mempty keqs [] mempty ebs xEnv
   where
-    keqs       = map (refine si qcs genv) ws `using` parList rdeepseq
+    keqs       = map (refine (solver cfg) si qcs genv) ws `using` parList rdeepseq
     qcs        = {- trace ("init-qs-size " ++ show (length ws, length qs_, M.keys qcs_)) $ -} qcs_
     qcs_       = mkQCluster qs_
     qs_        = F.quals si
@@ -80,8 +80,8 @@ qualSig q = [ p { F.qpSym = F.dummyName }  | p <- F.qParams q ]
 
 --------------------------------------------------------------------------------
 
-refine :: F.SInfo a -> QCluster -> F.SEnv F.Sort -> F.WfC a -> (F.KVar, Sol.QBind)
-refine info qs genv w = refineK (allowHOquals info) env qs (F.wrft w)
+refine :: SMTSolver -> F.SInfo a -> QCluster -> F.SEnv F.Sort -> F.WfC a -> (F.KVar, Sol.QBind)
+refine slv info qs genv w = refineK slv (allowHOquals info) env qs (F.wrft w)
   where
     env             = wenvSort <> genv
     wenvSort        = F.sr_sort <$> F.fromListSEnv (F.envCs (F.bs info) (F.wenv w))
@@ -92,11 +92,11 @@ instConstants = F.fromListSEnv . filter notLit . F.toListSEnv . F.gLits
     notLit    = not . F.isLitSymbol . fst
 
 
-refineK :: Bool -> F.SEnv F.Sort -> QCluster -> (F.Symbol, F.Sort, F.KVar) -> (F.KVar, Sol.QBind)
-refineK ho env qs (v, t, k) = F.notracepp _msg (k, eqs')
+refineK :: SMTSolver -> Bool -> F.SEnv F.Sort -> QCluster -> (F.Symbol, F.Sort, F.KVar) -> (F.KVar, Sol.QBind)
+refineK slv ho env qs (v, t, k) = F.notracepp _msg (k, eqs')
    where
     eqs                     = instK ho env v t qs
-    eqs'                    = Sol.qbFilter (okInst env v t) eqs
+    eqs'                    = Sol.qbFilter (okInst slv env v t) eqs
     _msg                    = printf "\n\nrefineK: k = %s, eqs = %s" (F.showpp k) (F.showpp eqs)
 
 --------------------------------------------------------------------------------
@@ -231,13 +231,13 @@ applyQPSubst _ p
   = p
 
 --------------------------------------------------------------------------------
-okInst :: F.SEnv F.Sort -> F.Symbol -> F.Sort -> Sol.EQual -> Bool
+okInst :: SMTSolver -> F.SEnv F.Sort -> F.Symbol -> F.Sort -> Sol.EQual -> Bool
 --------------------------------------------------------------------------------
-okInst env v t eq = isNothing tc
+okInst slv env v t eq = isNothing tc
   where
     sr            = F.RR t (F.Reft (v, p))
     p             = Sol.eqPred eq
-    tc            = So.checkSorted (F.srcSpan eq) env sr
+    tc            = So.checkSorted slv (F.srcSpan eq) env sr
     -- _msg          = printf "okInst: t = %s, eq = %s, env = %s" (F.showpp t) (F.showpp eq) (F.showpp env)
 
 
@@ -248,11 +248,12 @@ okInst env v t eq = isNothing tc
 lhsPred
   :: (F.Loc a)
   => F.IBindEnv
+  -> SMTSolver
   -> F.BindEnv a
   -> Sol.Solution
   -> F.SimpC a
   -> F.Expr
-lhsPred bindingsInSmt be s c = F.notracepp _msg $ fst $ apply g s bs
+lhsPred bindingsInSmt slv be s c = F.notracepp _msg $ fst $ apply slv g s bs
   where
     g          = CEnv ci be bs (F.srcSpan c) bindingsInSmt
     bs         = F.senv c
@@ -276,49 +277,49 @@ instance F.Loc (CombinedEnv a) where
 type Cid         = Maybe Integer
 type ExprInfo    = (F.Expr, KInfo)
 
-apply :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.IBindEnv -> ExprInfo
-apply g s bs      = (F.conj (pks:ps), kI)   -- see [NOTE: pAnd-SLOW]
+apply :: SMTSolver -> CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.IBindEnv -> ExprInfo
+apply slv g s bs      = (F.conj (pks:ps), kI)   -- see [NOTE: pAnd-SLOW]
   where
     -- Clear the "known" bindings for applyKVars, since it depends on
     -- using the fully expanded representation of the predicates to bind their
     -- variables with quantifiers.
-    (pks, kI)     = applyKVars g {ceBindingsInSmt = F.emptyIBindEnv} s ks
-    (ps,  ks, _)  = envConcKVars g s bs
+    (pks, kI)     = applyKVars slv g {ceBindingsInSmt = F.emptyIBindEnv} s ks
+    (ps,  ks, _)  = envConcKVars slv g s bs
 
 
-envConcKVars :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.IBindEnv -> ([F.Expr], [F.KVSub], [F.KVSub])
-envConcKVars g s bs = (concat pss, concat kss, L.nubBy (\x y -> F.ksuKVar x == F.ksuKVar y) $ concat gss)
+envConcKVars :: SMTSolver -> CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.IBindEnv -> ([F.Expr], [F.KVSub], [F.KVSub])
+envConcKVars slv g s bs = (concat pss, concat kss, L.nubBy (\x y -> F.ksuKVar x == F.ksuKVar y) $ concat gss)
   where
     (pss, kss, gss) = unzip3 [ F.notracepp ("sortedReftConcKVars" ++ F.showpp sr) $ F.sortedReftConcKVars x sr | (x, sr) <- xrs ]
-    xrs             = lookupBindEnvExt g s <$> is
+    xrs             = lookupBindEnvExt slv g s <$> is
     is              = F.elemsIBindEnv bs
 
-lookupBindEnvExt :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.BindId -> (F.Symbol, F.SortedReft)
-lookupBindEnvExt g s i
-  | Just p <- ebSol g {ceBindingsInSmt = F.emptyIBindEnv} s i = (x, sr { F.sr_reft = F.Reft (x, p) })
+lookupBindEnvExt :: SMTSolver -> CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.BindId -> (F.Symbol, F.SortedReft)
+lookupBindEnvExt slv g s i
+  | Just p <- ebSol slv g {ceBindingsInSmt = F.emptyIBindEnv} s i = (x, sr { F.sr_reft = F.Reft (x, p) })
   | F.memberIBindEnv i (ceBindingsInSmt g) =
       (x, sr { F.sr_reft = F.Reft (x, F.EVar (F.bindSymbol (fromIntegral i)))})
   | otherwise             = (x, sr)
    where
       (x, sr, _)              = F.lookupBindEnv i (ceBEnv g)
 
-ebSol :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.BindId -> Maybe F.Expr
-ebSol g sol bindId = case  M.lookup bindId sebds of
+ebSol :: SMTSolver -> CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.BindId -> Maybe F.Expr
+ebSol slv g sol bindId = case  M.lookup bindId sebds of
   Just (Sol.EbSol p)    -> Just p
   Just (Sol.EbDef cs _) -> Just $ F.PAnd (cSol <$> cs)
   _                     -> Nothing
   where
     sebds = Sol.sEbd sol
 
-    ebReft s (i,c) = exElim (Sol.sxEnv s) (senv c) i (ebindReft g s c)
+    ebReft s (i,c) = exElim (Sol.sxEnv s) (senv c) i (ebindReft slv g s c)
     cSol c = if sid c == ceCid g
                 then F.PFalse
                 else ebReft s' (bindId, c)
 
     s' = sol { Sol.sEbd = M.insert bindId Sol.EbIncr sebds }
 
-ebindReft :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.SimpC () -> F.Pred
-ebindReft g s c = F.pAnd [ fst $ apply g' s bs, F.crhs c ]
+ebindReft :: SMTSolver -> CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.SimpC () -> F.Pred
+ebindReft slv g s c = F.pAnd [ fst $ apply slv g' s bs, F.crhs c ]
   where
     g'          = g { ceCid = sid c, ceIEnv = bs }
     bs          = F.senv c
@@ -332,22 +333,22 @@ exElim env ienv xi p = F.notracepp msg (F.pExist yts p)
                             , xi < yi
                             , yi `F.memberIBindEnv` ienv                  ]
 
-applyKVars :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> [F.KVSub] -> ExprInfo
-applyKVars g s = mrExprInfos (applyKVar g s) F.pAndNoDedup mconcat
+applyKVars :: SMTSolver -> CombinedEnv ann -> Sol.Sol a Sol.QBind -> [F.KVSub] -> ExprInfo
+applyKVars slv g s = mrExprInfos (applyKVar slv g s) F.pAndNoDedup mconcat
 
-applyKVar :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> ExprInfo
-applyKVar g s ksu = case Sol.lookup s (F.ksuKVar ksu) of
-  Left cs   -> hypPred g s ksu cs
-  Right eqs -> (F.pAndNoDedup $ fst <$> Sol.qbPreds msg s (F.ksuSubst ksu) eqs, mempty) -- TODO: don't initialize kvars that have a hyp solution
+applyKVar :: SMTSolver -> CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> ExprInfo
+applyKVar slv g s ksu = case Sol.lookup s (F.ksuKVar ksu) of
+  Left cs   -> hypPred slv g s ksu cs
+  Right eqs -> (F.pAndNoDedup $ fst <$> Sol.qbPreds slv msg s (F.ksuSubst ksu) eqs, mempty) -- TODO: don't initialize kvars that have a hyp solution
   where
     msg     = "applyKVar: " ++ show (ceCid g)
 
-nonCutsResult :: F.BindEnv ann -> Sol.Sol a Sol.QBind -> M.HashMap F.KVar F.Expr
-nonCutsResult be s =
+nonCutsResult :: SMTSolver -> F.BindEnv ann -> Sol.Sol a Sol.QBind -> M.HashMap F.KVar F.Expr
+nonCutsResult slv be s =
   let g = CEnv Nothing be F.emptyIBindEnv F.dummySpan F.emptyIBindEnv
    in M.mapWithKey (mkNonCutsExpr g) $ Sol.sHyp s
   where
-    mkNonCutsExpr g k cs = F.pOr $ map (bareCubePred g s k) cs
+    mkNonCutsExpr g k cs = F.pOr $ map (bareCubePred slv g s k) cs
 
 -- | Produces a predicate from a constraint defining a kvar.
 --
@@ -366,20 +367,20 @@ nonCutsResult be s =
 --    particular use of the KVar. Thus @cubePred@ produces a different
 --    expression for every use site of the kvar, while here we produce one
 --    expression for all the uses.
-bareCubePred :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVar -> Sol.Cube -> F.Expr
-bareCubePred g s k c =
+bareCubePred :: SMTSolver -> CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVar -> Sol.Cube -> F.Expr
+bareCubePred slv g s k c =
   let bs = Sol.cuBinds c
       su = Sol.cuSubst c
       g' = addCEnv  g bs
       bs' = delCEnv s k bs
       yts = symSorts g bs'
       sEnv = F.seSort (Sol.sEnv s)
-      (xts, psu) = substElim (Sol.sEnv s) sEnv g' k su
-      (p, _kI) = apply g' s bs'
+      (xts, psu) = substElim slv (Sol.sEnv s) sEnv g' k su
+      (p, _kI) = apply slv g' s bs'
    in F.pExist (xts ++ yts) (psu &.& p)
 
-hypPred :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Hyp  -> ExprInfo
-hypPred g s ksu hyp = F.pOr *** mconcatPlus $ unzip $ cubePred g s ksu <$> hyp
+hypPred :: SMTSolver -> CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Hyp  -> ExprInfo
+hypPred slv g s ksu hyp = F.pOr *** mconcatPlus $ unzip $ cubePred slv g s ksu <$> hyp
 
 {- | `cubePred g s k su c` returns the predicate for
 
@@ -396,18 +397,18 @@ hypPred g s ksu hyp = F.pOr *** mconcatPlus $ unzip $ cubePred g s ksu <$> hyp
 
  -}
 
-elabExist :: F.SrcSpan -> Sol.Sol a Sol.QBind -> [(F.Symbol, F.Sort)] -> F.Expr -> F.Expr
-elabExist sp s xts p = F.pExist xts' p
+elabExist :: SMTSolver -> F.SrcSpan -> Sol.Sol a Sol.QBind -> [(F.Symbol, F.Sort)] -> F.Expr -> F.Expr
+elabExist slv sp s xts p = F.pExist xts' p
   where
     xts'        = [ (x, elab t) | (x, t) <- xts]
-    elab        = So.elaborate (F.atLoc sp "elabExist") env
+    elab        = So.elaborate slv (F.atLoc sp "elabExist") env
     env         = Sol.sEnv s
 
-cubePred :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Cube -> ExprInfo
-cubePred g s ksu c    = (F.notracepp "cubePred" $ elabExist sp s xts (psu &.& p), kI)
+cubePred :: SMTSolver -> CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Cube -> ExprInfo
+cubePred slv g s ksu c    = (F.notracepp "cubePred" $ elabExist slv sp s xts (psu &.& p), kI)
   where
     sp                = F.srcSpan g
-    ((xts,psu,p), kI) = cubePredExc g s ksu c bs'
+    ((xts,psu,p), kI) = cubePredExc slv g s ksu c bs'
     bs'               = delCEnv s k bs
     bs                = Sol.cuBinds c
     k                 = F.ksuKVar ksu
@@ -418,18 +419,18 @@ type Binders = [(F.Symbol, F.Sort)]
 --   The output is a tuple, `(xts, psu, p, kI)` such that the actual predicate
 --   we want is `Exists xts. (psu /\ p)`.
 
-cubePredExc :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Cube -> F.IBindEnv
+cubePredExc :: SMTSolver -> CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Cube -> F.IBindEnv
             -> ((Binders, F.Pred, F.Pred), KInfo)
 
-cubePredExc g s ksu c bs' = (cubeP, extendKInfo kI (Sol.cuTag c))
+cubePredExc slv g s ksu c bs' = (cubeP, extendKInfo kI (Sol.cuTag c))
   where
-    cubeP           = (xts, psu, elabExist sp s yts' (F.pAndNoDedup [p', psu']) )
+    cubeP           = (xts, psu, elabExist slv sp s yts' (F.pAndNoDedup [p', psu']) )
     sp              = F.srcSpan g
     yts'            = symSorts g bs'
     g'              = addCEnv  g bs
-    (p', kI)        = apply g' s bs'
-    (_  , psu')     = substElim (Sol.sEnv s) sEnv g' k su'
-    (xts, psu)      = substElim (Sol.sEnv s) sEnv g  k su
+    (p', kI)        = apply slv g' s bs'
+    (_  , psu')     = substElim slv (Sol.sEnv s) sEnv g' k su'
+    (xts, psu)      = substElim slv (Sol.sEnv s) sEnv g  k su
     su'             = Sol.cuSubst c
     bs              = Sol.cuBinds c
     k               = F.ksuKVar   ksu
@@ -462,10 +463,10 @@ cubePredExc g s ksu c bs' = (cubeP, extendKInfo kI (Sol.cuTag c))
      2. are binders corresponding to sorts (e.g. `a : num`, currently used
         to hack typeclasses current.)
  -}
-substElim :: F.SymEnv -> F.SEnv F.Sort -> CombinedEnv a -> F.KVar -> F.Subst -> ([(F.Symbol, F.Sort)], F.Pred)
-substElim syEnv sEnv g _ (F.Su m) = (xts, p)
+substElim :: SMTSolver -> F.SymEnv -> F.SEnv F.Sort -> CombinedEnv a -> F.KVar -> F.Subst -> ([(F.Symbol, F.Sort)], F.Pred)
+substElim slv syEnv sEnv g _ (F.Su m) = (xts, p)
   where
-    p      = F.pAnd [ mkSubst sp syEnv x (substSort sEnv frees x t) e t | (x, e, t) <- xets ]
+    p      = F.pAnd [ mkSubst slv sp syEnv x (substSort sEnv frees x t) e t | (x, e, t) <- xets ]
     xts    = [ (x, t)    | (x, _, t) <- xets, not (S.member x frees) ]
     xets   = [ (x, e, t) | (x, e)    <- xes, t <- sortOf e, not (isClass t)]
     xes    = M.toList m
@@ -481,19 +482,19 @@ substSort sEnv _frees sym _t = fromMaybe (err sym) $ F.lookupSEnv sym sEnv
 
 
 -- LH #1091
-mkSubst :: F.SrcSpan -> F.SymEnv -> F.Symbol -> F.Sort -> F.Expr -> F.Sort -> F.Expr
-mkSubst sp env x tx ey ty
+mkSubst :: SMTSolver -> F.SrcSpan -> F.SymEnv -> F.Symbol -> F.Sort -> F.Expr -> F.Sort -> F.Expr
+mkSubst slv sp env x tx ey ty
   | tx == ty    = F.EEq ex ey
   | otherwise   = {- F.tracepp _msg $ -} F.EEq ex' ey'
   where
     -- _msg        = "mkSubst-DIFF: tx = " ++ F.showpp tx ++ " ty = " ++ F.showpp ty
     --                                     ++ " ex' = " ++ F.showpp ex' ++ " ey' = " ++ F.showpp ey'
     ex          = F.expr x
-    ex'         = elabToInt sp env ex tx
-    ey'         = elabToInt sp env ey ty
+    ex'         = elabToInt slv sp env ex tx
+    ey'         = elabToInt slv sp env ey ty
 
-elabToInt :: F.SrcSpan -> F.SymEnv -> F.Expr -> F.Sort -> F.Expr
-elabToInt sp env e s = So.elaborate (F.atLoc sp "elabToInt") env (So.toInt env e s)
+elabToInt :: SMTSolver -> F.SrcSpan -> F.SymEnv -> F.Expr -> F.Sort -> F.Expr
+elabToInt slv sp env e s = So.elaborate slv (F.atLoc sp "elabToInt") env (So.toInt env e s)
 
 isClass :: F.Sort -> Bool
 isClass F.FNum  = True
diff --git a/src/Language/Fixpoint/Solver/Solve.hs b/src/Language/Fixpoint/Solver/Solve.hs
index fe4a699ab..996c99d6a 100644
--- a/src/Language/Fixpoint/Solver/Solve.hs
+++ b/src/Language/Fixpoint/Solver/Solve.hs
@@ -120,9 +120,10 @@ solve_ :: (NFData a, F.Fixpoint a, F.Loc a)
 solve_ cfg fi s0 ks wkl = do
   let s1   = F.notracepp "solve_ " $ {-# SCC "sol-init" #-} S.init cfg fi ks
   let s2   = mappend s0 s1
+  let slv  = solver cfg
   (s3, res0) <- sendConcreteBindingsToSMT F.emptyIBindEnv $ \bindingsInSmt -> do
     -- let s3   = solveEbinds fi s2
-    s3       <- {- SCC "sol-refine" -} refine bindingsInSmt s2 wkl
+    s3       <- {- SCC "sol-refine" -} refine bindingsInSmt slv s2 wkl
     res0     <- {- SCC "sol-result" -} result bindingsInSmt cfg wkl s3
     return (s3, res0)
 
@@ -130,7 +131,7 @@ solve_ cfg fi s0 ks wkl = do
     Unsafe _ bads | not (noLazyPLE cfg) && rewriteAxioms cfg && interpreter cfg -> do
       fi1 <- doInterpret cfg fi (map fst $ mytrace ("before the Interpreter " ++ show (length bads) ++ " constraints remain") bads)
       (s4, res1) <-  sendConcreteBindingsToSMT F.emptyIBindEnv $ \bindingsInSmt -> do
-        s4    <- {- SCC "sol-refine" -} refine bindingsInSmt s3 wkl
+        s4    <- {- SCC "sol-refine" -} refine bindingsInSmt slv s3 wkl
         res1  <- {- SCC "sol-result" -} result bindingsInSmt cfg wkl s4
         return (s4, res1)
       return (fi1, s4, res1)
@@ -140,7 +141,7 @@ solve_ cfg fi s0 ks wkl = do
     Unsafe _ bads2 | not (noLazyPLE cfg) && rewriteAxioms cfg -> do
       doPLE cfg fi1 (map fst $ mytrace ("before z3 PLE " ++ show (length bads2) ++ " constraints remain") bads2)
       sendConcreteBindingsToSMT F.emptyIBindEnv $ \bindingsInSmt -> do
-        s5    <- {- SCC "sol-refine" -} refine bindingsInSmt s4 wkl
+        s5    <- {- SCC "sol-refine" -} refine bindingsInSmt slv s4 wkl
         result bindingsInSmt cfg wkl s5
     _ -> return $ mytrace "all checked with interpreter" res1
 
@@ -170,17 +171,18 @@ tidyPred = F.substf (F.eVar . F.tidySymbol)
 refine
   :: (F.Loc a)
   => F.IBindEnv
+  -> SMTSolver
   -> Sol.Solution
   -> W.Worklist a
   -> SolveM a Sol.Solution
 --------------------------------------------------------------------------------
-refine bindingsInSmt s w
+refine bindingsInSmt slv s w
   | Just (c, w', newScc, rnk) <- W.pop w = do
      i       <- tickIter newScc
-     (b, s') <- refineC bindingsInSmt i s c
+     (b, s') <- refineC bindingsInSmt slv i s c
      lift $ writeLoud $ refineMsg i c b rnk (showpp s')
      let w'' = if b then W.push c w' else w'
-     refine bindingsInSmt s' w''
+     refine bindingsInSmt slv s' w''
   | otherwise = return s
   where
     -- DEBUG
@@ -194,31 +196,32 @@ refine bindingsInSmt s w
 refineC
   :: (F.Loc a)
   => F.IBindEnv
+  -> SMTSolver
   -> Int
   -> Sol.Solution
   -> F.SimpC a
   -> SolveM a (Bool, Sol.Solution)
 ---------------------------------------------------------------------------
-refineC bindingsInSmt _i s c
+refineC bindingsInSmt slv _i s c
   | null rhs  = return (False, s)
   | otherwise = do be     <- getBinds
-                   let lhs = S.lhsPred bindingsInSmt (F.coerceBindEnv be) s c
+                   let lhs = S.lhsPred bindingsInSmt slv (F.coerceBindEnv slv be) s c
                    kqs    <- filterValid (cstrSpan c) lhs rhs
                    return  $ S.update s ks kqs
   where
     _ci       = F.subcId c
-    (ks, rhs) = rhsCands s c
+    (ks, rhs) = rhsCands slv s c
     -- msg       = printf "refineC: iter = %d, sid = %s, soln = \n%s\n"
     --               _i (show (F.sid c)) (showpp s)
     _msg ks xs ys = printf "refineC: iter = %d, sid = %s, s = %s, rhs = %d, rhs' = %d \n"
                      _i (show _ci) (showpp ks) (length xs) (length ys)
 
-rhsCands :: Sol.Solution -> F.SimpC a -> ([F.KVar], Sol.Cand (F.KVar, Sol.EQual))
-rhsCands s c    = (fst <$> ks, kqs)
+rhsCands :: SMTSolver -> Sol.Solution -> F.SimpC a -> ([F.KVar], Sol.Cand (F.KVar, Sol.EQual))
+rhsCands slv s c    = (fst <$> ks, kqs)
   where
     kqs         = [ (p, (k, q)) | (k, su) <- ks, (p, q)  <- cnd k su ]
     ks          = predKs . F.crhs $ c
-    cnd k su    = Sol.qbPreds msg s su (Sol.lookupQBind s k)
+    cnd k su    = Sol.qbPreds slv msg s su (Sol.lookupQBind s k)
     msg         = "rhsCands: " ++ show (F.sid c)
 
 predKs :: F.Expr -> [(F.KVar, F.Subst)]
@@ -244,17 +247,17 @@ result bindingsInSmt cfg wkl s =
     stat    <- result_ bindingsInSmt2 cfg wkl s
     lift $ whenLoud $ putStrLn $ "RESULT: " ++ show (F.sid <$> stat)
 
-    F.Result (ci <$> stat) <$> solResult cfg s <*> solNonCutsResult s <*> return mempty
+    F.Result (ci <$> stat) <$> solResult cfg s <*> solNonCutsResult (solver cfg) s <*> return mempty
   where
     ci c = (F.subcId c, F.sinfo c)
 
 solResult :: Config -> Sol.Solution -> SolveM ann (M.HashMap F.KVar F.Expr)
 solResult cfg = minimizeResult cfg . Sol.result
 
-solNonCutsResult :: Sol.Solution -> SolveM ann (M.HashMap F.KVar F.Expr)
-solNonCutsResult s = do
+solNonCutsResult :: SMTSolver -> Sol.Solution -> SolveM ann (M.HashMap F.KVar F.Expr)
+solNonCutsResult slv s = do
   be <- getBinds
-  return $ S.nonCutsResult be s
+  return $ S.nonCutsResult slv be s
 
 result_
   :: (F.Loc a, NFData a)
@@ -264,7 +267,7 @@ result_
   -> Sol.Solution
   -> SolveM a (F.FixResult (F.SimpC a))
 result_ bindingsInSmt cfg w s = do
-  filtered <- filterM (isUnsat bindingsInSmt s) cs
+  filtered <- filterM (isUnsat bindingsInSmt (solver cfg) s) cs
   sts      <- stats
   pure $ res sts filtered
   where
@@ -305,13 +308,13 @@ minimizeConjuncts p = F.pAnd <$> go (F.conjuncts p) []
 
 --------------------------------------------------------------------------------
 isUnsat
-  :: (F.Loc a, NFData a) => F.IBindEnv -> Sol.Solution -> F.SimpC a -> SolveM a Bool
+  :: (F.Loc a, NFData a) => F.IBindEnv -> SMTSolver -> Sol.Solution -> F.SimpC a -> SolveM a Bool
 --------------------------------------------------------------------------------
-isUnsat bindingsInSmt s c = do
+isUnsat bindingsInSmt slv s c = do
   -- lift   $ printf "isUnsat %s" (show (F.subcId c))
   _     <- tickIter True -- newScc
   be    <- getBinds
-  let lp = S.lhsPred bindingsInSmt (F.coerceBindEnv be) s c
+  let lp = S.lhsPred bindingsInSmt slv (F.coerceBindEnv slv be) s c
   let rp = rhsPred        c
   res   <- not <$> isValid (cstrSpan c) lp rp
   lift   $ whenLoud $ showUnsat res (F.subcId c) lp rp
diff --git a/src/Language/Fixpoint/SortCheck.hs b/src/Language/Fixpoint/SortCheck.hs
index 42da843eb..edf7bff9d 100644
--- a/src/Language/Fixpoint/SortCheck.hs
+++ b/src/Language/Fixpoint/SortCheck.hs
@@ -80,6 +80,7 @@ import           Data.Maybe                (mapMaybe, fromMaybe, catMaybes, isJu
 import           Language.Fixpoint.Types.PrettyPrint
 import           Language.Fixpoint.Misc
 import           Language.Fixpoint.Types hiding   (subst, GInfo(..), senv)
+import qualified Language.Fixpoint.Types.Config as Cfg
 import qualified Language.Fixpoint.Types.Visitor  as Vis
 import qualified Language.Fixpoint.Smt.Theories   as Thy
 import           Text.PrettyPrint.HughesPJ.Compat
@@ -121,25 +122,25 @@ isMono             = null . Vis.foldSort fv []
 --   instantiated to `int` and `bool`.
 --------------------------------------------------------------------------------
 class Elaborate a where
-  elaborate :: Located String -> SymEnv -> a -> a
+  elaborate :: Cfg.SMTSolver -> Located String -> SymEnv -> a -> a
 
 
 instance (Loc a) => Elaborate (SInfo a) where
-  elaborate msg senv si = si
-    { F.cm      = elaborate msg senv <$> F.cm      si
-    , F.bs      = elaborate msg senv  $  F.bs      si
-    , F.asserts = elaborate msg senv <$> F.asserts si
+  elaborate slv msg senv si = si
+    { F.cm      = elaborate slv msg senv <$> F.cm      si
+    , F.bs      = elaborate slv msg senv  $  F.bs      si
+    , F.asserts = elaborate slv msg senv <$> F.asserts si
     }
 
 
 instance (Elaborate e) => (Elaborate (Triggered e)) where
-  elaborate msg env t = fmap (elaborate msg env) t
+  elaborate slv msg env t = fmap (elaborate slv msg env) t
 
 instance (Elaborate a) => (Elaborate (Maybe a)) where
-  elaborate msg env t = fmap (elaborate msg env) t
+  elaborate slv msg env t = fmap (elaborate slv msg env) t
 
 instance Elaborate Sort where
-  elaborate _ _ = go
+  elaborate _ _ _ = go
    where
       go s | isString s = strSort
       go (FAbs i s)    = FAbs i  (go s)
@@ -150,37 +151,37 @@ instance Elaborate Sort where
       funSort = FApp . FApp funcSort
 
 instance Elaborate AxiomEnv where
-  elaborate msg env ae = ae
-    { aenvEqs   = elaborate msg env (aenvEqs ae)
+  elaborate slv msg env ae = ae
+    { aenvEqs   = elaborate slv msg env (aenvEqs ae)
     -- MISSING SORTS OOPS, aenvSimpl = elaborate msg env (aenvSimpl ae)
     }
 
 instance Elaborate Rewrite where
-  elaborate msg env rw = rw { smBody = skipElabExpr msg env' (smBody rw) }
+  elaborate slv msg env rw = rw { smBody = skipElabExpr slv msg env' (smBody rw) }
     where
       env' = insertsSymEnv env undefined
 
 instance Elaborate Equation where
-  elaborate msg env eq = eq { eqBody = skipElabExpr msg env' (eqBody eq) }
+  elaborate slv msg env eq = eq { eqBody = skipElabExpr slv msg env' (eqBody eq) }
     where
       env' = insertsSymEnv env (eqArgs eq)
 
 instance Elaborate Expr where
-  elaborate msg env =
-    elabNumeric . elabApply env' . elabExpr msg env' . elabFSetMap
+  elaborate slv msg env =
+    elabNumeric . elabApply env' . elabExpr slv msg env' . elabFMap . (if Cfg.isZ3 slv then elabFSetBagZ3 else id)
       where
-        env' = coerceEnv env
+        env' = coerceEnv slv env
 
-skipElabExpr :: Located String -> SymEnv -> Expr -> Expr
-skipElabExpr msg env e = case elabExprE msg env e of
+skipElabExpr :: Cfg.SMTSolver -> Located String -> SymEnv -> Expr -> Expr
+skipElabExpr slv msg env e = case elabExprE slv msg env e of
   Left _   -> e
   Right e' -> elabNumeric . elabApply env $ e'
 
 instance Elaborate (Symbol, Sort) where
-  elaborate msg env (x, s) = (x, elaborate msg env s)
+  elaborate slv msg env (x, s) = (x, elaborate slv msg env s)
 
 instance Elaborate a => Elaborate [a]  where
-  elaborate msg env xs = elaborate msg env <$> xs
+  elaborate slv msg env xs = elaborate slv msg env <$> xs
 
 elabNumeric :: Expr -> Expr
 elabNumeric = Vis.mapExprOnExpr go
@@ -197,83 +198,110 @@ elabNumeric = Vis.mapExprOnExpr go
       = e
 
 instance Elaborate SortedReft where
-  elaborate msg env (RR s (Reft (v, e))) = RR s (Reft (v, e'))
+  elaborate slv msg env (RR s (Reft (v, e))) = RR s (Reft (v, e'))
     where
-      e'   = elaborate msg env' e
+      e'   = elaborate slv msg env' e
       env' = insertSymEnv v s env
 
 instance (Loc a) => Elaborate (BindEnv a) where
-  elaborate msg env = mapBindEnv (\i (x, sr, l) -> (x, elaborate (msg' l i x sr) env sr, l))
+  elaborate slv msg env = mapBindEnv (\i (x, sr, l) -> (x, elaborate slv (msg' l i x sr) env sr, l))
     where
       msg' l i x sr = atLoc l (val msg ++ unwords [" elabBE", show i, show x, show sr])
 
 instance (Loc a) => Elaborate (SimpC a) where
-  elaborate msg env c = c {_crhs = elaborate msg' env (_crhs c) }
+  elaborate slv msg env c = c {_crhs = elaborate slv msg' env (_crhs c) }
     where msg'        = atLoc c (val msg)
 
 
---------------------------------------------------------------------------------------------------
--- | 'elabFSetMap' replaces all finset/finmap/finbag theory operations with array-based encodings.
---------------------------------------------------------------------------------------------------
-elabFSetMap :: Expr -> Expr
-elabFSetMap (EApp h@(EVar f) e)
-  | f == Thy.setEmpty      = EApp (EVar Thy.arrConstS) PFalse
-  | f == Thy.setEmp        = PAtom Eq (EApp (EVar Thy.arrConstS) PFalse) (elabFSetMap e)
-  | f == Thy.setSng        = EApp (EApp (EApp (EVar Thy.arrStoreS) (EApp (EVar Thy.arrConstS) PFalse)) (elabFSetMap e)) PTrue
-  | f == Thy.setCom        = EApp (EVar Thy.arrMapNotS) (elabFSetMap e)
-  | f == Thy.mapDef        = EApp (EVar Thy.arrConstM) (elabFSetMap e)
-  | f == Thy.bagEmpty      = EApp (EVar Thy.arrConstB) (ECon (I 0))
-  | otherwise              = EApp (elabFSetMap h) (elabFSetMap e)
-elabFSetMap (EApp (EApp h@(EVar f) e1) e2)
-  | f == Thy.setMem        = EApp (EApp (EVar Thy.arrSelectS) (elabFSetMap e2)) (elabFSetMap e1)
-  | f == Thy.setCup        = EApp (EApp (EVar Thy.arrMapOrS) (elabFSetMap e1)) (elabFSetMap e2)
-  | f == Thy.setCap        = EApp (EApp (EVar Thy.arrMapAndS) (elabFSetMap e1)) (elabFSetMap e2)
-  | f == Thy.setAdd        = EApp (EApp (EApp (EVar Thy.arrStoreS) (elabFSetMap e1)) (elabFSetMap e2)) PTrue
+-----------------------------------------------------------------------------------
+-- | Replace all finset/finmap/finbag theory operations with array-based encodings.
+-----------------------------------------------------------------------------------
+
+-- TODO there's no actual elaboration happening here, just symbol renaming
+elabFMap :: Expr -> Expr
+elabFMap (EApp h@(EVar f) e)
+  | f == Thy.mapDef        = EApp (EVar Thy.arrConstM) (elabFMap e)
+  | otherwise              = EApp (elabFMap h) (elabFMap e)
+elabFMap (EApp (EApp h@(EVar f) e1) e2)
+  | f == Thy.mapSel        = EApp (EApp (EVar Thy.arrSelectM) (elabFMap e1)) (elabFMap e2)
+  | otherwise              = EApp (EApp (elabFMap h) (elabFMap e1)) (elabFMap e2)
+elabFMap (EApp (EApp (EApp h@(EVar f) e1) e2) e3)
+  | f == Thy.mapSto        = EApp (EApp (EApp (EVar Thy.arrStoreM) (elabFMap e1)) (elabFMap e2)) (elabFMap e3)
+  | otherwise              = EApp (EApp (EApp (elabFMap h) (elabFMap e1)) (elabFMap e2)) (elabFMap e3)
+elabFMap (EApp e1 e2)      = EApp (elabFMap e1) (elabFMap e2)
+elabFMap (ENeg e)          = ENeg (elabFMap e)
+elabFMap (EBin b e1 e2)    = EBin b (elabFMap e1) (elabFMap e2)
+elabFMap (EIte e1 e2 e3)   = EIte (elabFMap e1) (elabFMap e2) (elabFMap e3)
+elabFMap (ECst e t)        = ECst (elabFMap e) t
+elabFMap (ELam b e)        = ELam b (elabFMap e)
+elabFMap (ETApp e t)       = ETApp (elabFMap e) t
+elabFMap (ETAbs e t)       = ETAbs (elabFMap e) t
+elabFMap (PAnd es)         = PAnd (elabFMap <$> es)
+elabFMap (POr es)          = POr (elabFMap <$> es)
+elabFMap (PNot e)          = PNot (elabFMap e)
+elabFMap (PImp e1 e2)      = PImp (elabFMap e1) (elabFMap e2)
+elabFMap (PIff e1 e2)      = PIff (elabFMap e1) (elabFMap e2)
+elabFMap (PAtom r e1 e2)   = PAtom r (elabFMap e1) (elabFMap e2)
+elabFMap (PAll   bs e)     = PAll bs (elabFMap e)
+elabFMap (PExist bs e)     = PExist bs (elabFMap e)
+elabFMap (PGrad  k su i e) = PGrad k su i (elabFMap e)
+elabFMap (ECoerc a t e)    = ECoerc a t (elabFMap e)
+elabFMap e                 = e
+
+elabFSetBagZ3 :: Expr -> Expr
+elabFSetBagZ3 (EApp h@(EVar f) e)
+  | f == Thy.setEmpty         = EApp (EVar Thy.arrConstS) PFalse
+  | f == Thy.setEmp           = PAtom Eq (EApp (EVar Thy.arrConstS) PFalse) (elabFSetBagZ3 e)
+  | f == Thy.setSng           = EApp (EApp (EApp (EVar Thy.arrStoreS) (EApp (EVar Thy.arrConstS) PFalse)) (elabFSetBagZ3 e)) PTrue
+  | f == Thy.setCom           = EApp (EVar Thy.arrMapNotS) (elabFSetBagZ3 e)
+  | f == Thy.bagEmpty         = EApp (EVar Thy.arrConstB) (ECon (I 0))
+  | otherwise                 = EApp (elabFSetBagZ3 h) (elabFSetBagZ3 e)
+elabFSetBagZ3 (EApp (EApp h@(EVar f) e1) e2)
+  | f == Thy.setMem           = EApp (EApp (EVar Thy.arrSelectS) (elabFSetBagZ3 e2)) (elabFSetBagZ3 e1)
+  | f == Thy.setCup           = EApp (EApp (EVar Thy.arrMapOrS) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2)
+  | f == Thy.setCap           = EApp (EApp (EVar Thy.arrMapAndS) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2)
+  | f == Thy.setAdd           = EApp (EApp (EApp (EVar Thy.arrStoreS) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2)) PTrue
   -- A \ B == A /\ ~B == ~(A => B)
-  | f == Thy.setDif        = EApp (EApp (EVar Thy.arrMapAndS) (elabFSetMap e1)) (EApp (EVar Thy.arrMapNotS) (elabFSetMap e2))
-  | f == Thy.setSub        = PAtom Eq (EApp (EVar Thy.arrConstS) PTrue) (EApp (EApp (EVar Thy.arrMapImpS) (elabFSetMap e1)) (elabFSetMap e2))
-  | f == Thy.mapSel        = EApp (EApp (EVar Thy.arrSelectM) (elabFSetMap e1)) (elabFSetMap e2)
-  | f == Thy.bagCount      = EApp (EApp (EVar Thy.arrSelectB) (elabFSetMap e1)) (elabFSetMap e2)
-  | f == Thy.bagSng        = EApp (EApp (EApp (EVar Thy.arrStoreB) (EApp (EVar Thy.arrConstB) (ECon (I 0)))) (elabFSetMap e1)) (elabFSetMap e2)
-  | f == Thy.bagCup        = EApp (EApp (EVar Thy.arrMapPlusB) (elabFSetMap e1)) (elabFSetMap e2)
-  | f == Thy.bagSub        = PAtom Eq (EApp (EVar Thy.arrConstS) PTrue) (EApp (EApp (EVar Thy.arrMapLeB) (elabFSetMap e1)) (elabFSetMap e2))
-  | f == Thy.bagMax        = EApp (EApp (EApp (EVar Thy.arrMapIteB) (EApp (EApp (EVar Thy.arrMapGtB) (elabFSetMap e1)) (elabFSetMap e2))) (elabFSetMap e1)) (elabFSetMap e2)
-  | f == Thy.bagMin        = EApp (EApp (EApp (EVar Thy.arrMapIteB) (EApp (EApp (EVar Thy.arrMapLeB) (elabFSetMap e1)) (elabFSetMap e2))) (elabFSetMap e1)) (elabFSetMap e2)
-  | otherwise              = EApp (EApp (elabFSetMap h) (elabFSetMap e1)) (elabFSetMap e2)
-elabFSetMap (EApp (EApp (EApp h@(EVar f) e1) e2) e3)
-  | f == Thy.mapSto        = EApp (EApp (EApp (EVar Thy.arrStoreM) (elabFSetMap e1)) (elabFSetMap e2)) (elabFSetMap e3)
-  | otherwise              = EApp (EApp (EApp (elabFSetMap h) (elabFSetMap e1)) (elabFSetMap e2)) (elabFSetMap e3)
-elabFSetMap (EApp e1 e2)      = EApp (elabFSetMap e1) (elabFSetMap e2)
-elabFSetMap (ENeg e)          = ENeg (elabFSetMap e)
-elabFSetMap (EBin b e1 e2)    = EBin b (elabFSetMap e1) (elabFSetMap e2)
-elabFSetMap (EIte e1 e2 e3)   = EIte (elabFSetMap e1) (elabFSetMap e2) (elabFSetMap e3)
-elabFSetMap (ECst e t)        = ECst (elabFSetMap e) t
-elabFSetMap (ELam b e)        = ELam b (elabFSetMap e)
-elabFSetMap (ETApp e t)       = ETApp (elabFSetMap e) t
-elabFSetMap (ETAbs e t)       = ETAbs (elabFSetMap e) t
-elabFSetMap (PAnd es)         = PAnd (elabFSetMap <$> es)
-elabFSetMap (POr es)          = POr (elabFSetMap <$> es)
-elabFSetMap (PNot e)          = PNot (elabFSetMap e)
-elabFSetMap (PImp e1 e2)      = PImp (elabFSetMap e1) (elabFSetMap e2)
-elabFSetMap (PIff e1 e2)      = PIff (elabFSetMap e1) (elabFSetMap e2)
-elabFSetMap (PAtom r e1 e2)   = PAtom r (elabFSetMap e1) (elabFSetMap e2)
-elabFSetMap (PAll   bs e)     = PAll bs (elabFSetMap e)
-elabFSetMap (PExist bs e)     = PExist bs (elabFSetMap e)
-elabFSetMap (PGrad  k su i e) = PGrad k su i (elabFSetMap e)
-elabFSetMap (ECoerc a t e)    = ECoerc a t (elabFSetMap e)
-elabFSetMap e                 = e
+  | f == Thy.setDif           = EApp (EApp (EVar Thy.arrMapAndS) (elabFSetBagZ3 e1)) (EApp (EVar Thy.arrMapNotS) (elabFSetBagZ3 e2))
+  | f == Thy.setSub           = PAtom Eq (EApp (EVar Thy.arrConstS) PTrue) (EApp (EApp (EVar Thy.arrMapImpS) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2))
+  | f == Thy.bagCount         = EApp (EApp (EVar Thy.arrSelectB) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2)
+  | f == Thy.bagSng           = EApp (EApp (EApp (EVar Thy.arrStoreB) (EApp (EVar Thy.arrConstB) (ECon (I 0)))) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2)
+  | f == Thy.bagCup           = EApp (EApp (EVar Thy.arrMapPlusB) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2)
+  | f == Thy.bagSub           = PAtom Eq (EApp (EVar Thy.arrConstS) PTrue) (EApp (EApp (EVar Thy.arrMapLeB) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2))
+  | f == Thy.bagMax           = EApp (EApp (EApp (EVar Thy.arrMapIteB) (EApp (EApp (EVar Thy.arrMapGtB) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2))) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2)
+  | f == Thy.bagMin           = EApp (EApp (EApp (EVar Thy.arrMapIteB) (EApp (EApp (EVar Thy.arrMapLeB) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2))) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2)
+  | otherwise                 = EApp (EApp (elabFSetBagZ3 h) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2)
+elabFSetBagZ3 (EApp e1 e2)      = EApp (elabFSetBagZ3 e1) (elabFSetBagZ3 e2)
+elabFSetBagZ3 (ENeg e)          = ENeg (elabFSetBagZ3 e)
+elabFSetBagZ3 (EBin b e1 e2)    = EBin b (elabFSetBagZ3 e1) (elabFSetBagZ3 e2)
+elabFSetBagZ3 (EIte e1 e2 e3)   = EIte (elabFSetBagZ3 e1) (elabFSetBagZ3 e2) (elabFSetBagZ3 e3)
+elabFSetBagZ3 (ECst e t)        = ECst (elabFSetBagZ3 e) t
+elabFSetBagZ3 (ELam b e)        = ELam b (elabFSetBagZ3 e)
+elabFSetBagZ3 (ETApp e t)       = ETApp (elabFSetBagZ3 e) t
+elabFSetBagZ3 (ETAbs e t)       = ETAbs (elabFSetBagZ3 e) t
+elabFSetBagZ3 (PAnd es)         = PAnd (elabFSetBagZ3 <$> es)
+elabFSetBagZ3 (POr es)          = POr (elabFSetBagZ3 <$> es)
+elabFSetBagZ3 (PNot e)          = PNot (elabFSetBagZ3 e)
+elabFSetBagZ3 (PImp e1 e2)      = PImp (elabFSetBagZ3 e1) (elabFSetBagZ3 e2)
+elabFSetBagZ3 (PIff e1 e2)      = PIff (elabFSetBagZ3 e1) (elabFSetBagZ3 e2)
+elabFSetBagZ3 (PAtom r e1 e2)   = PAtom r (elabFSetBagZ3 e1) (elabFSetBagZ3 e2)
+elabFSetBagZ3 (PAll   bs e)     = PAll bs (elabFSetBagZ3 e)
+elabFSetBagZ3 (PExist bs e)     = PExist bs (elabFSetBagZ3 e)
+elabFSetBagZ3 (PGrad  k su i e) = PGrad k su i (elabFSetBagZ3 e)
+elabFSetBagZ3 (ECoerc a t e)    = ECoerc a t (elabFSetBagZ3 e)
+elabFSetBagZ3 e                 = e
 
 --------------------------------------------------------------------------------
 -- | 'elabExpr' adds "casts" to decorate polymorphic instantiation sites.
 --------------------------------------------------------------------------------
-elabExpr :: Located String -> SymEnv -> Expr -> Expr
-elabExpr msg env e = case elabExprE msg env e of
+elabExpr :: Cfg.SMTSolver -> Located String -> SymEnv -> Expr -> Expr
+elabExpr slv msg env e = case elabExprE slv msg env e of
   Left ex  -> die ex
   Right e' -> F.notracepp ("elabExp " ++ showpp e) e'
 
-elabExprE :: Located String -> SymEnv -> Expr -> Either Error Expr
-elabExprE msg env e =
-  case runCM0 (srcSpan msg) (elab (env, envLookup) e) of
+elabExprE :: Cfg.SMTSolver -> Located String -> SymEnv -> Expr -> Either Error Expr
+elabExprE slv msg env e =
+  case runCM0 (srcSpan msg) (elab slv (env, envLookup) e) of
     Left (ChError f') ->
       let e' = f' ()
        in Left $ err (srcSpan e') (d (val e'))
@@ -423,25 +451,25 @@ checkSortedReft env xs sr = applyNonNull Nothing oops unknowns
     unknowns              = [ x | x <- syms sr, x `notElem` v : xs, not (x `memberSEnv` env)]
     Reft (v,_)            = sr_reft sr
 
-checkSortedReftFull :: Checkable a => SrcSpan -> SEnv SortedReft -> a -> Maybe Doc
-checkSortedReftFull sp γ t =
-  case runCM0 sp (check γ' t) of
+checkSortedReftFull :: Checkable a => Cfg.SMTSolver -> SrcSpan -> SEnv SortedReft -> a -> Maybe Doc
+checkSortedReftFull slv sp γ t =
+  case runCM0 sp (check slv γ' t) of
     Left (ChError f)  -> Just (text (val (f ())))
     Right _ -> Nothing
   where
     γ' = sr_sort <$> γ
 
-checkSortFull :: Checkable a => SrcSpan -> SEnv SortedReft -> Sort -> a -> Maybe Doc
-checkSortFull sp γ s t =
-  case runCM0 sp (checkSort γ' s t) of
+checkSortFull :: Checkable a => Cfg.SMTSolver -> SrcSpan -> SEnv SortedReft -> Sort -> a -> Maybe Doc
+checkSortFull slv sp γ s t =
+  case runCM0 sp (checkSort slv γ' s t) of
     Left (ChError f)  -> Just (text (val (f ())))
     Right _ -> Nothing
   where
       γ' = sr_sort <$> γ
 
-checkSorted :: Checkable a => SrcSpan -> SEnv Sort -> a -> Maybe Doc
-checkSorted sp γ t =
-  case runCM0 sp (check γ t) of
+checkSorted :: Checkable a => Cfg.SMTSolver -> SrcSpan -> SEnv Sort -> a -> Maybe Doc
+checkSorted slv sp γ t =
+  case runCM0 sp (check slv γ t) of
     Left (ChError f)  -> Just (text (val (f ())))
     Right _  -> Nothing
 
@@ -471,20 +499,22 @@ checkPred' f p = res -- traceFix ("checkPred: p = " ++ showFix p) $ res
                    Right _   -> Just p
 
 class Checkable a where
-  check     :: SEnv Sort -> a -> CheckM ()
-  checkSort :: SEnv Sort -> Sort -> a -> CheckM ()
+  check     :: Cfg.SMTSolver -> SEnv Sort -> a -> CheckM ()
+  checkSort :: Cfg.SMTSolver -> SEnv Sort -> Sort -> a -> CheckM ()
 
-  checkSort γ _ = check γ
+  checkSort slv γ _ = check slv γ
 
 instance Checkable Expr where
-  check γ e = void $ checkExpr f e
-   where f = (`lookupSEnvWithDistance` coerceSortEnv γ)
+  check slv γ e = void $ checkExpr f e
+   where f = (`lookupSEnvWithDistance` coerceSortEnv slv γ)
 
-  checkSort γ s e = void $ checkExpr f (ECst e (coerceSetMapToArray s))
-   where f = (`lookupSEnvWithDistance` coerceSortEnv γ)
+  checkSort slv γ s e = void $ checkExpr f (ECst e (if Cfg.isZ3 slv then coerceSetBagToArray s' else s'))
+   where
+      s' = coerceMapToArray s
+      f = (`lookupSEnvWithDistance` coerceSortEnv slv γ)
 
 instance Checkable SortedReft where
-  check γ (RR s (Reft (v, ra))) = check γ' ra
+  check slv γ (RR s (Reft (v, ra))) = check slv γ' ra
    where
      γ' = insertSEnv v s γ
 
@@ -528,146 +558,146 @@ addEnv f bs x
 -- | Elaborate expressions with types to make polymorphic instantiation explicit.
 --------------------------------------------------------------------------------
 {-# SCC elab #-}
-elab :: ElabEnv -> Expr -> CheckM (Expr, Sort)
+elab :: Cfg.SMTSolver -> ElabEnv -> Expr -> CheckM (Expr, Sort)
 --------------------------------------------------------------------------------
-elab f@(_, g) e@(EBin o e1 e2) = do
-  (e1', s1) <- elab f e1
-  (e2', s2) <- elab f e2
+elab slv f@(_, g) e@(EBin o e1 e2) = do
+  (e1', s1) <- elab slv f e1
+  (e2', s2) <- elab slv f e2
   s <- checkOpTy g e s1 s2
   return (EBin o (eCst e1' s1) (eCst e2' s2), s)
 
-elab f (EApp e1@(EApp _ _) e2) = do
-  (e1', _, e2', s2, s) <- notracepp "ELAB-EAPP" <$> elabEApp f e1 e2
+elab slv f (EApp e1@(EApp _ _) e2) = do
+  (e1', _, e2', s2, s) <- notracepp "ELAB-EAPP" <$> elabEApp slv f e1 e2
   let e = eAppC s e1' (eCst e2' s2)
   let θ = unifyExpr (snd f) e
   return (applyExpr θ e, maybe s (`apply` s) θ)
 
-elab f (EApp e1 e2) = do
-  (e1', s1, e2', s2, s) <- elabEApp f e1 e2
+elab slv f (EApp e1 e2) = do
+  (e1', s1, e2', s2, s) <- elabEApp slv f e1 e2
   let e = eAppC s (eCst e1' s1) (eCst e2' s2)
   let θ = unifyExpr (snd f) e
   return (applyExpr θ e, maybe s (`apply` s) θ)
 
-elab _ e@(ESym _) =
+elab _ _ e@(ESym _) =
   return (e, strSort)
 
-elab _ e@(ECon (I _)) =
+elab _ _ e@(ECon (I _)) =
   return (e, FInt)
 
-elab _ e@(ECon (R _)) =
+elab _ _ e@(ECon (R _)) =
   return (e, FReal)
 
-elab _ e@(ECon (L _ s)) =
+elab _ _ e@(ECon (L _ s)) =
   return (e, s)
 
-elab _ e@(PKVar _ _) =
+elab _ _ e@(PKVar _ _) =
   return (e, boolSort)
 
-elab f (PGrad k su i e) =
-  (, boolSort) . PGrad k su i . fst <$> elab f e
+elab slv f (PGrad k su i e) =
+  (, boolSort) . PGrad k su i . fst <$> elab slv f e
 
-elab (_, f) e@(EVar x) = do
+elab _ (_, f) e@(EVar x) = do
   cs <- checkSym f x
   pure (e, cs)
 
-elab f (ENeg e) = do
-  (e', s) <- elab f e
+elab slv f (ENeg e) = do
+  (e', s) <- elab slv f e
   return (ENeg e', s)
 
-elab f@(_,g) (ECst (EIte p e1 e2) t) = do
-  (p', _)   <- elab f p
-  (e1', s1) <- elab f (eCst e1 t)
-  (e2', s2) <- elab f (eCst e2 t)
+elab slv f@(_,g) (ECst (EIte p e1 e2) t) = do
+  (p', _)   <- elab slv f p
+  (e1', s1) <- elab slv f (eCst e1 t)
+  (e2', s2) <- elab slv f (eCst e2 t)
   s         <- checkIteTy g p e1' e2' s1 s2
   return (EIte p' (eCst e1' s) (eCst e2' s), t)
 
-elab f@(_,g) (EIte p e1 e2) = do
+elab slv f@(_,g) (EIte p e1 e2) = do
   t <- getIte g e1 e2
-  (p', _)   <- elab f p
-  (e1', s1) <- elab f (eCst e1 t)
-  (e2', s2) <- elab f (eCst e2 t)
+  (p', _)   <- elab slv f p
+  (e1', s1) <- elab slv f (eCst e1 t)
+  (e2', s2) <- elab slv f (eCst e2 t)
   s         <- checkIteTy g p e1' e2' s1 s2
   return (EIte p' (eCst e1' s) (eCst e2' s), s)
 
-elab f (ECst e t) = do
-  (e', _) <- elab f e
+elab slv f (ECst e t) = do
+  (e', _) <- elab slv f e
   return (eCst e' t, t)
 
-elab f (PNot p) = do
-  (e', _) <- elab f p
+elab slv f (PNot p) = do
+  (e', _) <- elab slv f p
   return (PNot e', boolSort)
 
-elab f (PImp p1 p2) = do
-  (p1', _) <- elab f p1
-  (p2', _) <- elab f p2
+elab slv f (PImp p1 p2) = do
+  (p1', _) <- elab slv f p1
+  (p2', _) <- elab slv f p2
   return (PImp p1' p2', boolSort)
 
-elab f (PIff p1 p2) = do
-  (p1', _) <- elab f p1
-  (p2', _) <- elab f p2
+elab slv f (PIff p1 p2) = do
+  (p1', _) <- elab slv f p1
+  (p2', _) <- elab slv f p2
   return (PIff p1' p2', boolSort)
 
-elab f (PAnd ps) = do
-  ps' <- mapM (elab f) ps
+elab slv f (PAnd ps) = do
+  ps' <- mapM (elab slv f) ps
   return (PAnd (fst <$> ps'), boolSort)
 
-elab f (POr ps) = do
-  ps' <- mapM (elab f) ps
+elab slv f (POr ps) = do
+  ps' <- mapM (elab slv f) ps
   return (POr (fst <$> ps'), boolSort)
 
-elab f@(_,g) e@(PAtom eq e1 e2) | eq == Eq || eq == Ne = do
+elab slv f@(_,g) e@(PAtom eq e1 e2) | eq == Eq || eq == Ne = do
   t1        <- checkExpr g e1
   t2        <- checkExpr g e2
   (t1',t2') <- unite g e t1 t2 `withError` errElabExpr e
-  e1'       <- elabAs f t1' e1
-  e2'       <- elabAs f t2' e2
-  e1''      <- eCstAtom f e1' t1'
-  e2''      <- eCstAtom f e2' t2'
+  e1'       <- elabAs slv f t1' e1
+  e2'       <- elabAs slv f t2' e2
+  e1''      <- eCstAtom slv f e1' t1'
+  e2''      <- eCstAtom slv f e2' t2'
   return (PAtom eq e1'' e2'' , boolSort)
 
-elab f (PAtom r e1 e2)
+elab slv f (PAtom r e1 e2)
   | r == Ueq || r == Une = do
-  (e1', _) <- elab f e1
-  (e2', _) <- elab f e2
+  (e1', _) <- elab slv f e1
+  (e2', _) <- elab slv f e2
   return (PAtom r e1' e2', boolSort)
 
-elab f@(env,_) (PAtom r e1 e2) = do
-  e1' <- uncurry (toInt env) <$> elab f e1
-  e2' <- uncurry (toInt env) <$> elab f e2
+elab slv f@(env,_) (PAtom r e1 e2) = do
+  e1' <- uncurry (toInt env) <$> elab slv f e1
+  e2' <- uncurry (toInt env) <$> elab slv f e2
   return (PAtom r e1' e2', boolSort)
 
-elab f (PExist bs e) = do
-  (e', s) <- elab (elabAddEnv f bs) e
-  let bs' = elaborate "PExist Args" mempty bs
+elab slv f (PExist bs e) = do
+  (e', s) <- elab slv (elabAddEnv f bs) e
+  let bs' = elaborate slv "PExist Args" mempty bs
   return (PExist bs' e', s)
 
-elab f (PAll bs e) = do
-  (e', s) <- elab (elabAddEnv f bs) e
-  let bs' = elaborate "PAll Args" mempty bs
+elab slv f (PAll bs e) = do
+  (e', s) <- elab slv (elabAddEnv f bs) e
+  let bs' = elaborate slv "PAll Args" mempty bs
   return (PAll bs' e', s)
 
-elab f (ELam (x,t) e) = do
-  (e', s) <- elab (elabAddEnv f [(x, t)]) e
-  let t' = elaborate "ELam Arg" mempty t
+elab slv f (ELam (x,t) e) = do
+  (e', s) <- elab slv (elabAddEnv f [(x, t)]) e
+  let t' = elaborate slv "ELam Arg" mempty t
   return (ELam (x, t') (eCst e' s), FFunc t s)
 
-elab f (ECoerc s t e) = do
-  (e', _) <- elab f e
+elab slv f (ECoerc s t e) = do
+  (e', _) <- elab slv f e
   return     (ECoerc s t e', t)
 
-elab _ (ETApp _ _) =
+elab _ _ (ETApp _ _) =
   error "SortCheck.elab: TODO: implement ETApp"
-elab _ (ETAbs _ _) =
+elab _ _ (ETAbs _ _) =
   error "SortCheck.elab: TODO: implement ETAbs"
 
 
 -- | 'eCstAtom' is to support tests like `tests/pos/undef00.fq`
-eCstAtom :: ElabEnv -> Expr -> Sort -> CheckM Expr
-eCstAtom f@(sym,g) (EVar x) t
+eCstAtom :: Cfg.SMTSolver -> ElabEnv -> Expr -> Sort -> CheckM Expr
+eCstAtom slv f@(sym,g) (EVar x) t
   | Found s <- g x
   , isUndef s
-  , not (isNum sym t) = (`ECst` t) <$> elabAs f t (EApp (eVar tyCastName) (eVar x))
-eCstAtom _ e t = return (ECst e t)
+  , not (isNum sym t) = (`ECst` t) <$> elabAs slv f t (EApp (eVar tyCastName) (eVar x))
+eCstAtom _ _ e t = return (ECst e t)
 
 isUndef :: Sort -> Bool
 isUndef s = case bkAbs s of
@@ -678,31 +708,31 @@ isUndef s = case bkAbs s of
 elabAddEnv :: Eq a => (t, a -> SESearch b) -> [(a, b)] -> (t, a -> SESearch b)
 elabAddEnv (g, f) bs = (g, addEnv f bs)
 
-elabAs :: ElabEnv -> Sort -> Expr -> CheckM Expr
-elabAs f t e = notracepp _msg <$> go e
+elabAs :: Cfg.SMTSolver -> ElabEnv -> Sort -> Expr -> CheckM Expr
+elabAs slv f t e = notracepp _msg <$> go e
   where
     _msg  = "elabAs: t = " ++ showpp t ++ "; e = " ++ showpp e
-    go (EApp e1 e2) = elabAppAs f t e1 e2
-    go e'           = fst <$> elab f e'
+    go (EApp e1 e2) = elabAppAs slv f t e1 e2
+    go e'           = fst <$> elab slv f e'
 
 -- DUPLICATION with `checkApp'`
-elabAppAs :: ElabEnv -> Sort -> Expr -> Expr -> CheckM Expr
-elabAppAs env@(_, f) t g e = do
+elabAppAs :: Cfg.SMTSolver -> ElabEnv -> Sort -> Expr -> Expr -> CheckM Expr
+elabAppAs slv env@(_, f) t g e = do
   gT       <- checkExpr f g
   eT       <- checkExpr f e
   (iT, oT, isu) <- checkFunSort gT
   let ge    = Just (EApp g e)
   su       <- unifyMany f ge isu [oT, iT] [t, eT]
   let tg    = apply su gT
-  g'       <- elabAs env tg g
+  g'       <- elabAs slv env tg g
   let te    = apply su eT
-  e'       <- elabAs env te e
+  e'       <- elabAs slv env te e
   pure     $ EApp (ECst g' tg) (ECst e' te)
 
-elabEApp  :: ElabEnv -> Expr -> Expr -> CheckM (Expr, Sort, Expr, Sort, Sort)
-elabEApp f@(_, g) e1 e2 = do
-  (e1', s1)     <- {- notracepp ("elabEApp: e1 = " ++ show e1) <$> -} elab f e1
-  (e2', s2)     <- {- notracepp ("elabEApp: e2 = " ++ show e2) <$> -} elab f e2
+elabEApp  :: Cfg.SMTSolver -> ElabEnv -> Expr -> Expr -> CheckM (Expr, Sort, Expr, Sort, Sort)
+elabEApp slv f@(_, g) e1 e2 = do
+  (e1', s1)     <- {- notracepp ("elabEApp: e1 = " ++ show e1) <$> -} elab slv f e1
+  (e2', s2)     <- {- notracepp ("elabEApp: e2 = " ++ show e2) <$> -} elab slv f e2
   (e1'', e2'', s1', s2', s) <- elabAppSort g e1' e2' s1 s2
   return           (e1'', s1', e2'', s2', s)
 
@@ -908,7 +938,7 @@ which, I imagine is what happens _somewhere_ inside GHC too?
 --------------------------------------------------------------------------------
 applySorts :: Vis.Visitable t => t -> [Sort]
 --------------------------------------------------------------------------------
-applySorts = {- notracepp "applySorts" . -} (defs ++) . Vis.fold vis () []
+applySorts = {- tracepp "applySorts" . -} (defs ++) . Vis.fold vis () []
   where
     defs   = [FFunc t1 t2 | t1 <- basicSorts, t2 <- basicSorts]
     vis    = (Vis.defaultVisitor :: Vis.Visitor [KVar] t) { Vis.accExpr = go }
@@ -970,7 +1000,7 @@ refreshNegativeTyVars s = do
     let negativeSorts = negSort s
     freshVars <- mapM pair $ S.toList negativeSorts
     pure $ foldr (uncurry subst) s freshVars
-  where 
+  where
     pair i = do
       f <- fresh
       pure (i, FVar f)
diff --git a/src/Language/Fixpoint/Types/Config.hs b/src/Language/Fixpoint/Types/Config.hs
index 6487c5986..4890bbad5 100644
--- a/src/Language/Fixpoint/Types/Config.hs
+++ b/src/Language/Fixpoint/Types/Config.hs
@@ -13,6 +13,7 @@ module Language.Fixpoint.Types.Config (
 
   -- * SMT Solver options
   , SMTSolver (..)
+  , isZ3
 
   -- REST Options
   , RESTOrdering (..)
@@ -146,9 +147,14 @@ instance Read RESTOrdering where
 
 ---------------------------------------------------------------------------------------
 
-data SMTSolver = Z3 | Z3mem | Cvc4 | Cvc5 | Mathsat 
+data SMTSolver = Z3 | Z3mem | Cvc4 | Cvc5 | Mathsat
                  deriving (Eq, Data, Typeable, Generic)
 
+isZ3 :: SMTSolver -> Bool
+isZ3 Z3    = True
+isZ3 Z3mem = True
+isZ3 _     = False
+
 instance Default SMTSolver where
   def = if Conditional.Z3.builtWithZ3AsALibrary then Z3mem else Z3
 
diff --git a/src/Language/Fixpoint/Types/Environments.hs b/src/Language/Fixpoint/Types/Environments.hs
index 27b966122..15d5ef53d 100644
--- a/src/Language/Fixpoint/Types/Environments.hs
+++ b/src/Language/Fixpoint/Types/Environments.hs
@@ -73,6 +73,7 @@ import           Data.Function             (on)
 import           Text.PrettyPrint.HughesPJ.Compat
 import           Control.DeepSeq
 
+import           Language.Fixpoint.Types.Config
 import           Language.Fixpoint.Types.PrettyPrint
 import           Language.Fixpoint.Types.Names
 import           Language.Fixpoint.Types.Sorts
@@ -368,5 +369,8 @@ makePack kvss = Packs (M.fromList kIs)
     kIs       = [ (k, i) | (i, ks) <- kPacks, k <- ks ]
     kPacks    = zip [0..] . coalesce . fmap S.toList $ kvss
 
-coerceBindEnv :: BindEnv a -> BindEnv a
-coerceBindEnv be = be { beBinds = M.map (\(s, sr, a) -> (s, sr { sr_sort = coerceSetMapToArray (sr_sort sr) } , a)) (beBinds be) }
+coerceBindEnv :: SMTSolver -> BindEnv a -> BindEnv a
+coerceBindEnv slv be = be { beBinds = M.map (\(s, sr, a) ->
+                                                let srs = coerceMapToArray (sr_sort sr) in
+                                                (s, sr { sr_sort = if isZ3 slv then coerceSetBagToArray srs else srs } , a))
+                                            (beBinds be) }
diff --git a/src/Language/Fixpoint/Types/Graduals.hs b/src/Language/Fixpoint/Types/Graduals.hs
index 6e5577383..9a48af4ab 100644
--- a/src/Language/Fixpoint/Types/Graduals.hs
+++ b/src/Language/Fixpoint/Types/Graduals.hs
@@ -230,30 +230,30 @@ expandWF km ws
 -------------------------------------------------------------------------------
 
 class Gradual a where
-  gsubst :: GSol -> a -> a
+  gsubst :: SMTSolver -> GSol -> a -> a
 
 instance Gradual Expr where
-  gsubst (GSol env m) e   = mapGVars' (\(k, _) -> Just (fromMaybe (err k) (mknew k))) e
+  gsubst slv (GSol env m) e   = mapGVars' (\(k, _) -> Just (fromMaybe (err k) (mknew k))) e
     where
-      mknew k = So.elaborate "initBGind.mkPred" env $ fst <$> M.lookup k m
+      mknew k = So.elaborate slv "initBGind.mkPred" env $ fst <$> M.lookup k m
       err   k = errorstar ("gradual substitution: Cannot find " ++ showpp k)
 
 instance Gradual Reft where
-  gsubst su (Reft (x, e)) = Reft (x, gsubst su e)
+  gsubst slv su (Reft (x, e)) = Reft (x, gsubst slv su e)
 
 instance Gradual SortedReft where
-  gsubst su r = r {sr_reft = gsubst su (sr_reft r)}
+  gsubst slv su r = r {sr_reft = gsubst slv su (sr_reft r)}
 
 instance Gradual (SimpC a) where
-  gsubst su c = c {_crhs = gsubst su (_crhs c)}
+  gsubst slv su c = c {_crhs = gsubst slv su (_crhs c)}
 
 instance Gradual (BindEnv a) where
-  gsubst su = mapBindEnv (\_ (x, r, l) -> (x, gsubst su r, l))
+  gsubst slv su = mapBindEnv (\_ (x, r, l) -> (x, gsubst slv su r, l))
 
 instance Gradual v => Gradual (M.HashMap k v) where
-  gsubst su = M.map (gsubst su)
+  gsubst slv su = M.map (gsubst slv su)
 
 instance Gradual (SInfo a) where
-  gsubst su fi = fi { bs = gsubst su (bs fi)
-                    , cm = gsubst su (cm fi)
-                    }
+  gsubst slv su fi = fi { bs = gsubst slv su (bs fi)
+                        , cm = gsubst slv su (cm fi)
+                        }
diff --git a/src/Language/Fixpoint/Types/Solutions.hs b/src/Language/Fixpoint/Types/Solutions.hs
index 00c374840..8b9280593 100644
--- a/src/Language/Fixpoint/Types/Solutions.hs
+++ b/src/Language/Fixpoint/Types/Solutions.hs
@@ -85,6 +85,7 @@ import           Data.Typeable             (Typeable)
 import           Control.Monad (filterM)
 import           Language.Fixpoint.Misc
 import           Language.Fixpoint.Types.PrettyPrint
+import           Language.Fixpoint.Types.Config  as Cfg
 import           Language.Fixpoint.Types.Spans
 import           Language.Fixpoint.Types.Names
 import           Language.Fixpoint.Types.Sorts
@@ -306,11 +307,11 @@ fromList env kGs kXs kYs z ebs xbs
     ebm = M.fromList ebs
 
 --------------------------------------------------------------------------------
-qbPreds :: String -> Sol a QBind -> Subst -> QBind -> [(Pred, EQual)]
+qbPreds :: Cfg.SMTSolver -> String -> Sol a QBind -> Subst -> QBind -> [(Pred, EQual)]
 --------------------------------------------------------------------------------
-qbPreds msg s su (QB eqs) = [ (elabPred eq, eq) | eq <- eqs ]
+qbPreds slv msg s su (QB eqs) = [ (elabPred eq, eq) | eq <- eqs ]
   where
-    elabPred eq           = elaborate (atLoc eq $ "qbPreds:" ++ msg) env
+    elabPred eq           = elaborate slv (atLoc eq $ "qbPreds:" ++ msg) env
                           . subst su
                           . eqPred
                           $ eq
diff --git a/src/Language/Fixpoint/Types/Sorts.hs b/src/Language/Fixpoint/Types/Sorts.hs
index 9ab613933..47c7b25e9 100644
--- a/src/Language/Fixpoint/Types/Sorts.hs
+++ b/src/Language/Fixpoint/Types/Sorts.hs
@@ -85,7 +85,8 @@ module Language.Fixpoint.Types.Sorts (
   , tceMap
 
   -- * Sort coercion for SMT theory encoding
-  , coerceSetMapToArray
+  , coerceMapToArray
+  , coerceSetBagToArray
   ) where
 
 import qualified Data.Store as S
@@ -685,17 +686,23 @@ tceMember :: (Eq a, Hashable a) => a -> TCEmb a -> Bool
 tceMember k (TCE m) = M.member k m
 
 -------------------------------------------------------------------------------
--- | Sort coercion for Z3 SMT theory encoding
+-- | Sort coercion for SMT theory encoding
 -------------------------------------------------------------------------------
 
-coerceSetMapToArray :: Sort -> Sort
-coerceSetMapToArray (FFunc sf sa) = FFunc (coerceSetMapToArray sf) (coerceSetMapToArray sa)
-coerceSetMapToArray (FAbs i sa)   = FAbs i (coerceSetMapToArray sa)
-coerceSetMapToArray (FApp (FApp sf sa) sb)
-  | isMap sf = arraySort (coerceSetMapToArray sa) (coerceSetMapToArray sb)
-  | otherwise = FApp (FApp (coerceSetMapToArray sf) (coerceSetMapToArray sa)) (coerceSetMapToArray sb)
-coerceSetMapToArray (FApp sf sa)
-  | isSet sf = arraySort (coerceSetMapToArray sa) boolSort
-  | isBag sf = arraySort (coerceSetMapToArray sa) intSort
-  | otherwise = FApp (coerceSetMapToArray sf) (coerceSetMapToArray sa)
-coerceSetMapToArray s = s
+coerceMapToArray :: Sort -> Sort
+coerceMapToArray (FFunc sf sa) = FFunc (coerceMapToArray sf) (coerceMapToArray sa)
+coerceMapToArray (FAbs i sa)   = FAbs i (coerceMapToArray sa)
+coerceMapToArray (FApp (FApp sf sa) sb)
+  | isMap sf = arraySort (coerceMapToArray sa) (coerceMapToArray sb)
+  | otherwise = FApp (FApp (coerceMapToArray sf) (coerceMapToArray sa)) (coerceMapToArray sb)
+coerceMapToArray (FApp sf sa) = FApp (coerceMapToArray sf) (coerceMapToArray sa)
+coerceMapToArray s = s
+
+coerceSetBagToArray :: Sort -> Sort
+coerceSetBagToArray (FFunc sf sa) = FFunc (coerceSetBagToArray sf) (coerceSetBagToArray sa)
+coerceSetBagToArray (FAbs i sa)   = FAbs i (coerceSetBagToArray sa)
+coerceSetBagToArray (FApp sf sa)
+  | isSet sf = arraySort (coerceSetBagToArray sa) boolSort
+  | isBag sf = arraySort (coerceSetBagToArray sa) intSort
+  | otherwise = FApp (coerceSetBagToArray sf) (coerceSetBagToArray sa)
+coerceSetBagToArray s = s
diff --git a/src/Language/Fixpoint/Types/Theories.hs b/src/Language/Fixpoint/Types/Theories.hs
index 529d9fcf8..81bf59178 100644
--- a/src/Language/Fixpoint/Types/Theories.hs
+++ b/src/Language/Fixpoint/Types/Theories.hs
@@ -45,6 +45,7 @@ import           Data.Typeable             (Typeable)
 import           Data.Hashable
 import           GHC.Generics              (Generic)
 import           Control.DeepSeq
+import           Language.Fixpoint.Types.Config
 import           Language.Fixpoint.Types.PrettyPrint
 import           Language.Fixpoint.Types.Names
 import           Language.Fixpoint.Types.Sorts
@@ -140,7 +141,7 @@ funcSorts :: SEnv DataDecl -> [Sort] -> [FuncSort]
 funcSorts dEnv ts = [ (t1, t2) | t1 <- smts, t2 <- smts]
   where
     smts = Misc.sortNub $ concat [ tx t1 ++ tx t2 | FFunc t1 t2 <- ts ]
-    tx   = inlineArr False dEnv
+    tx   = inlineArrSetBag False dEnv
 
 -- Related to the above, after merging #688, we now allow types other than
 -- Int to which Sets/Bags/Maps (or Arrays in the case of Z3) can be applied.
@@ -155,8 +156,8 @@ funcSorts dEnv ts = [ (t1, t2) | t1 <- smts, t2 <- smts]
 -- solution should be implemented for generating ad-hoc sets of applys on the
 -- fly, as described above.
 
-inlineArr :: Bool -> SEnv DataDecl -> Sort -> [SmtSort]
-inlineArr isArr env t  = go . unAbs $ t
+inlineArrSetBag :: Bool -> SEnv DataDecl -> Sort -> [SmtSort]
+inlineArrSetBag isASB env t  = go . unAbs $ t
   where
     m = sortAbs t
     go (FFunc _ _)    = [SInt]
@@ -166,19 +167,23 @@ inlineArr isArr env t  = go . unAbs $ t
       | t == boolSort = [SBool]
       | isString t    = [SString]
     go (FVar _)
-      | isArr     = SInt : map (\q -> let dd = snd q in
+      | isASB     = SInt : map (\q -> let dd = snd q in
                                       SData (ddTyCon dd) (replicate (ddVars dd) SInt))
                                (M.toList $ seBinds env)
       | otherwise = [SInt]
     go t
-      | (ct:ts) <- unFApp t = inlineArrFApp m env ct ts
+      | (ct:ts) <- unFApp t = inlineArrSetBagFApp m env ct ts
       | otherwise = error "Unexpected empty 'unFApp t'"
 
-inlineArrFApp :: Int -> SEnv DataDecl -> Sort -> [Sort] -> [SmtSort]
-inlineArrFApp m env = go
+inlineArrSetBagFApp :: Int -> SEnv DataDecl -> Sort -> [Sort] -> [SmtSort]
+inlineArrSetBagFApp m env = go
   where
+    go (FTC c) [a]
+      | setConName == symbol c   = SSet <$> inlineArrSetBag True env a
+    go (FTC c) [a]
+      | bagConName == symbol c   = SBag <$> inlineArrSetBag True env a
     go (FTC c) [a, b]
-      | arrayConName == symbol c = SArray <$> inlineArr True env a <*> inlineArr True env b
+      | arrayConName == symbol c = SArray <$> inlineArrSetBag True env a <*> inlineArrSetBag True env b
     go (FTC bv) [FTC s]
       | bitVecName == symbol bv
       , Just n <- sizeBv s      = [SBitVec n]
@@ -186,7 +191,7 @@ inlineArrFApp m env = go
       | isString s              = [SString]
     go (FTC c) ts
       | Just n <- tyArgs c env
-      , let i = n - length ts   = [SData c ((inlineArr False env . FAbs m =<< ts) ++ replicate i SInt)]
+      , let i = n - length ts   = [SData c ((inlineArrSetBag False env . FAbs m =<< ts) ++ replicate i SInt)]
     go _ _                      = [SInt]
 
 
@@ -281,9 +286,8 @@ data SmtSort
   | SBool
   | SReal
   | SString
-  -- TODO bring these back when adding CVC5 support
-  -- | SSet
-  -- | SMap
+  | SSet !SmtSort
+  | SBag !SmtSort
   | SArray !SmtSort !SmtSort
   | SBitVec !Int
   | SVar    !Int
@@ -323,10 +327,10 @@ fappSmtSort poly m env = go
   where
 -- HKT    go t@(FVar _) ts            = SApp (sortSmtSort poly env <$> (t:ts))
 
-    --go (FTC c) _
-    --  | setConName == symbol c  = SSet
-    --go (FTC c) _
-    --  | mapConName == symbol c  = SMap
+    go (FTC c) [a]
+      | setConName == symbol c  = SSet (sortSmtSort poly env a)
+    go (FTC c) [a]
+      | bagConName == symbol c  = SBag (sortSmtSort poly env a)
     go (FTC c) [a, b]
       | arrayConName == symbol c = SArray (sortSmtSort poly env a) (sortSmtSort poly env b)
     go (FTC bv) [FTC s]
@@ -350,8 +354,8 @@ instance PPrint SmtSort where
   pprintTidy _ SBool        = text "Bool"
   pprintTidy _ SReal        = text "Real"
   pprintTidy _ SString      = text "Str"
-  --pprintTidy _ SSet         = text "Set"
-  --pprintTidy _ SMap         = text "Map"
+  pprintTidy k (SSet a)     = ppParens k (text "Set") [a]
+  pprintTidy k (SBag a)     = ppParens k (text "Bag") [a]
   pprintTidy k (SArray a b) = ppParens k (text "Array") [a, b]
   pprintTidy _ (SBitVec n)  = text "BitVec" <+> int n
   pprintTidy _ (SVar i)     = text "@" <-> int i
@@ -365,13 +369,13 @@ ppParens k d ds = parens $ Misc.intersperse (text "") (d : (pprintTidy k <$> ds)
 -- | Coercing sorts inside environments for SMT theory encoding
 --------------------------------------------------------------------------------
 
-coerceSortEnv :: SEnv Sort -> SEnv Sort
-coerceSortEnv ss = coerceSetMapToArray <$> ss
+coerceSortEnv :: SMTSolver -> SEnv Sort -> SEnv Sort
+coerceSortEnv slv ss = (if isZ3 slv then coerceSetBagToArray else id) . coerceMapToArray <$> ss
 
-coerceEnv :: SymEnv -> SymEnv
-coerceEnv env = SymEnv { seSort   = coerceSortEnv (seSort env)
-                       , seTheory = seTheory env
-                       , seData   = seData   env
-                       , seLits   = seLits   env
-                       , seAppls  = seAppls  env
-                       }
\ No newline at end of file
+coerceEnv :: SMTSolver -> SymEnv -> SymEnv
+coerceEnv slv env = SymEnv { seSort   = coerceSortEnv slv (seSort env)
+                           , seTheory = seTheory env
+                           , seData   = seData   env
+                           , seLits   = seLits   env
+                           , seAppls  = seAppls  env
+                           }
\ No newline at end of file
diff --git a/tests/test.hs b/tests/test.hs
index e3c4c1a2b..ec54d7421 100644
--- a/tests/test.hs
+++ b/tests/test.hs
@@ -94,6 +94,7 @@ unitTests lfDir
     , testGroup "elim-pos2"  <$> dirTests elimCmd   "tests/elim"   []             ExitSuccess
     , testGroup "elim-neg"   <$> dirTests elimCmd   "tests/neg"    ["float.fq"]   (ExitFailure 1)
     , testGroup "elim-crash" <$> dirTests elimCmd   "tests/crash"  []             (ExitFailure 1)
+    , testGroup "cvc5-pos"   <$> dirTests cvc5SaveCmd   "tests/pos"    skipNativePos  ExitSuccess
     , testGroup "proof"      <$> dirTests elimCmd   "tests/proof"     []          ExitSuccess
     , testGroup "rankN"      <$> dirTests elimCmd   "tests/rankNTypes" []         ExitSuccess
     , testGroup "horn-pos-el"      <$> dirTests elimSaveCmd   "tests/horn/pos"  []          ExitSuccess
@@ -193,6 +194,10 @@ cvc5Cmd :: TestCmd
 cvc5Cmd (LO opts) bin dir file =
   printf "cd %s && %s --solver=cvc5 %s %s" dir bin opts file
 
+cvc5SaveCmd :: TestCmd
+cvc5SaveCmd (LO opts) bin dir file =
+  printf "cd %s && %s --save --solver=cvc5 %s %s" dir bin opts file
+
 ----------------------------------------------------------------------------------------
 -- Generic Helpers
 ----------------------------------------------------------------------------------------