diff --git a/liquid-fixpoint.cabal b/liquid-fixpoint.cabal
--- a/liquid-fixpoint.cabal
+++ b/liquid-fixpoint.cabal
@@ -1,6 +1,6 @@
 cabal-version:      2.4
 name:               liquid-fixpoint
-version:            0.9.0.2.1
+version:            0.9.2.5
 synopsis:           Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
 description:
   This package implements an SMTLIB based Horn-Clause\/Logical Implication constraint
@@ -41,6 +41,11 @@
   type: git
   location: https://github.com/ucsd-progsys/liquid-fixpoint
 
+flag link-z3-as-a-library
+  description: link z3 as a library for faster interactions with the SMT solver
+  manual: True
+  default: False
+
 flag devel
   description: turn on stricter error reporting for development
   manual: True
@@ -49,6 +54,7 @@
 library
   import: warnings
   exposed-modules:  Data.ShareMap
+                    Language.Fixpoint.Conditional.Z3
                     Language.Fixpoint.Defunctionalize
                     Language.Fixpoint.Graph
                     Language.Fixpoint.Graph.Deps
@@ -64,7 +70,6 @@
                     Language.Fixpoint.Minimize
                     Language.Fixpoint.Misc
                     Language.Fixpoint.Parse
-                    Language.Fixpoint.Smt.Bitvector
                     Language.Fixpoint.Smt.Interface
                     Language.Fixpoint.Smt.Serialize
                     Language.Fixpoint.Smt.Theories
@@ -128,7 +133,7 @@
                   , base                 >= 4.9.1.0 && < 5
                   , binary
                   , boxes
-                  , bytestring
+                  , bytestring >= 0.10.2.1
                   , cereal
                   , cmdargs
                   , containers
@@ -145,7 +150,10 @@
                   , parser-combinators
                   , pretty               >= 1.1.3.1
                   , process
+                  , typed-process
                   , rest-rewrite >= 0.3.0
+                  , smtlib-backends >= 0.3
+                  , smtlib-backends-process >= 0.3
                   , stm
                   , store
                   , vector < 0.13
@@ -156,6 +164,11 @@
   ghc-options:
     -fwrite-ide-info
     -hiedir=.hie
+  if flag(link-z3-as-a-library)
+    build-depends: smtlib-backends-z3 >= 0.3
+    hs-source-dirs: src-cond/with-z3
+  else
+    hs-source-dirs: src-cond/without-z3
 
   if flag(devel)
     ghc-options: -Werror
@@ -193,9 +206,10 @@
                   , mtl           >= 2.2.2
                   , optparse-applicative
                   , process
+                  , typed-process
                   , stm           >= 2.4
                   , tagged
-                  , tasty         >= 0.10
+                  , tasty         >= 0.10 && < 1.5
                   , tasty-ant-xml
                   , tasty-hunit   >= 0.9
                   , tasty-rerun   >= 1.1.12
diff --git a/src-cond/with-z3/Language/Fixpoint/Conditional/Z3.hs b/src-cond/with-z3/Language/Fixpoint/Conditional/Z3.hs
new file mode 100644
--- /dev/null
+++ b/src-cond/with-z3/Language/Fixpoint/Conditional/Z3.hs
@@ -0,0 +1,12 @@
+module Language.Fixpoint.Conditional.Z3 where
+
+import qualified SMTLIB.Backends
+import qualified SMTLIB.Backends.Z3 as Z3
+
+makeZ3 :: IO (SMTLIB.Backends.Backend, IO ())
+makeZ3 = do
+    handle <- Z3.new Z3.defaultConfig
+    return (Z3.toBackend handle, Z3.close handle)
+
+builtWithZ3AsALibrary :: Bool
+builtWithZ3AsALibrary = True
diff --git a/src-cond/without-z3/Language/Fixpoint/Conditional/Z3.hs b/src-cond/without-z3/Language/Fixpoint/Conditional/Z3.hs
new file mode 100644
--- /dev/null
+++ b/src-cond/without-z3/Language/Fixpoint/Conditional/Z3.hs
@@ -0,0 +1,7 @@
+module Language.Fixpoint.Conditional.Z3 where
+
+makeZ3 :: IO a
+makeZ3 = error "liquid-fixpoint: Not built with the Z3 backend. Please, enable the cabal flag link-z3-as-a-library."
+
+builtWithZ3AsALibrary :: Bool
+builtWithZ3AsALibrary = False
diff --git a/src/Language/Fixpoint/Horn/Info.hs b/src/Language/Fixpoint/Horn/Info.hs
--- a/src/Language/Fixpoint/Horn/Info.hs
+++ b/src/Language/Fixpoint/Horn/Info.hs
@@ -5,6 +5,7 @@
     hornFInfo
   ) where
 
+import           Control.Monad (forM)
 import qualified Data.HashMap.Strict            as M
 import qualified Data.List                      as L
 import qualified Data.Tuple                     as Tuple
@@ -14,7 +15,7 @@
 import qualified Language.Fixpoint.Types        as F
 import qualified Language.Fixpoint.Types.Config as F
 import qualified Language.Fixpoint.Horn.Types   as H
-import Data.Maybe (fromMaybe)
+import qualified Data.Maybe                     as Mb
 
 hornFInfo :: F.Config -> H.Query a -> F.FInfo a
 hornFInfo cfg q = mempty
@@ -22,7 +23,7 @@
   , F.bs        = be2
   , F.ebinds    = ebs
   , F.ws        = kvEnvWfCs kve
-  , F.quals     = H.qQuals q
+  , F.quals     = H.qQuals q ++ scrapeCstr (F.scrape cfg) hCst
   , F.gLits     = F.fromMapSEnv $ H.qCon q
   , F.dLits     = F.fromMapSEnv $ H.qDis q
   , F.ae        = axEnv cfg q cs
@@ -34,6 +35,7 @@
     (be2, ebs, cs) = hornSubCs be1 kve hCst
     hCst           = H.qCstr q
 
+
 axEnv :: F.Config -> H.Query a -> M.HashMap F.SubcId b -> F.AxiomEnv
 axEnv cfg q cs = mempty
   { F.aenvEqs    = H.qEqns q
@@ -89,7 +91,7 @@
 myMkSubC :: F.IBindEnv -> Maybe F.SortedReft -> F.SortedReft -> Maybe Integer -> F.Tag -> a -> F.SubC a
 myMkSubC be lhsMb rhs x y z = F.mkSubC be lhs rhs x y z
   where
-    lhs = fromMaybe def lhsMb
+    lhs = Mb.fromMaybe def lhsMb
     def = F.trueSortedReft (F.sr_sort rhs)
 
 bindSortedReft :: KVEnv a -> H.Bind a -> F.SortedReft
@@ -102,10 +104,6 @@
                  Just (F.RR ss (F.Reft (vv, _))) -> (ss, vv)
                  Nothing                       -> (F.intSort, F.dummySymbol)
 
--- dummyBind :: a -> Bind a
--- dummyBind = Bind F.dummySymbol F.intSort (PAnd [])
-
-
 predExpr :: KVEnv a -> H.Pred -> F.Expr
 predExpr kve        = go
   where
@@ -166,3 +164,95 @@
 
 hvarPrefix :: F.Symbol
 hvarPrefix = F.symbol "nnf_arg"
+
+-------------------------------------------------------------------------------
+-- | Automatically scrape qualifiers from all predicates in a constraint
+-------------------------------------------------------------------------------
+
+scrapeCstr :: F.Scrape -> H.Cstr a -> [F.Qualifier]
+scrapeCstr F.No _    = []
+scrapeCstr m    cstr = Misc.sortNub $ go emptyBindEnv cstr
+  where
+    go senv (H.Head p _) = scrapePred senv p
+    go senv (H.CAnd cs)  = concatMap (go senv) cs
+    go senv (H.All b c)  = scrapeBind m senv' b <> go senv' c where senv' = insertBindEnv b senv
+    go senv (H.Any b c)  = scrapeBind m senv' b <> go senv' c where senv' = insertBindEnv b senv
+
+scrapeBind :: F.Scrape -> BindEnv -> H.Bind a -> [F.Qualifier]
+scrapeBind F.Both senv b = scrapePred senv (H.bPred b)
+scrapeBind _      _    _ = []
+
+scrapePred :: BindEnv -> H.Pred -> [F.Qualifier]
+scrapePred _    (H.Var _ _) = []
+scrapePred senv (H.PAnd ps) = concatMap (scrapePred senv) ps
+scrapePred senv (H.Reft e)  = concatMap (mkQual senv) (F.concConjuncts e)
+
+-- NOTE: Constraints.mkQual will do extra stuff like generalizing the sorts...
+mkQual :: BindEnv -> F.Expr -> [ F.Qualifier ]
+mkQual env e = case qualParams env e of
+  Nothing  -> []
+  Just xts -> [ mkScrapeQual xts' e | xts' <- shiftCycle xts ]
+
+mkScrapeQual :: [(F.Symbol, F.Sort)] -> F.Expr -> F.Qualifier
+mkScrapeQual xts e = F.mkQual (F.symbol "AUTO") qParams (F.subst su e) (F.dummyPos "")
+  where
+    qParams = [ F.QP {F.qpSym = y, F.qpPat = F.PatNone, F.qpSort = t} | (_, y, t) <- xyts ]
+    xyts    = zipWith (\i (x, t) -> (x, F.bindSymbol i, t)) [0..] xts
+    su      = F.mkSubst [ (x, F.expr y) | (x, y, _) <- xyts ]
+
+
+shiftCycle :: [(F.Symbol, F.Sort)] -> [[(F.Symbol, F.Sort)]]
+shiftCycle xts
+  | n <= maxQualifierParams = recycle n xts
+  | otherwise              = []
+  where
+    n                      = length xts
+
+recycle :: Int -> [a] -> [[a]]
+recycle 0 _      = []
+recycle _ []     = []
+recycle k (x:xs) = (x:xs) : recycle (k-1) (xs ++ [x])
+
+maxQualifierParams :: Int
+maxQualifierParams = 3
+
+{-
+  1. Normalize the names
+  2. Permute the args?
+ -}
+
+qualParams :: BindEnv -> F.Expr -> Maybe [(F.Symbol, F.Sort)]
+qualParams env e = do
+    let xs = Misc.nubOrd (F.syms e)
+    ixts <- forM xs $ \x -> do
+              (t, i) <- lookupBindEnv x env
+              return (i, x, t)
+    return [ (x, t) | (_, x, t) <- reverse . L.sort $ ixts ]
+
+    -- ixts = [ (i, x, t) | x <- xs, (i, t) <- lookupBindEnv x env ]
+
+-------------------------------------------------------------------------------
+
+-- | `BindEnv` maps each symbol to (sort, depth) pair, where shorter depths
+--    means bound "earlier" i.e. in (forall (x1:...) (forall (x2:...) ...)
+--    the depth of x1 is less than the depth of x2.
+--    We use the heuristic that the symbol with the "largest" depth is the
+--    "value-variable" in the qualifier.
+
+data BindEnv = BindEnv
+  { bSize  :: !Int
+  , bBinds :: M.HashMap F.Symbol (F.Sort, Int)
+  }
+
+emptyBindEnv :: BindEnv
+emptyBindEnv = BindEnv { bSize = 0, bBinds = mempty }
+
+insertBindEnv :: H.Bind a -> BindEnv -> BindEnv
+insertBindEnv b senv = BindEnv { bSize = n + 1, bBinds = M.insert x (t, n) (bBinds senv) }
+  where
+    n = bSize senv
+    x = H.bSym b
+    t = H.bSort b
+
+lookupBindEnv :: F.Symbol -> BindEnv -> Maybe (F.Sort, Int)
+lookupBindEnv x env = M.lookup x (bBinds env)
diff --git a/src/Language/Fixpoint/Horn/Parse.hs b/src/Language/Fixpoint/Horn/Parse.hs
--- a/src/Language/Fixpoint/Horn/Parse.hs
+++ b/src/Language/Fixpoint/Horn/Parse.hs
@@ -50,6 +50,7 @@
   | HMat  F.Rewrite
   | HDat !F.DataDecl
   | HOpt !String
+  | HNum ()
   deriving (Functor)
 
 hThingP :: Parser (HThing H.Tag)
@@ -64,6 +65,12 @@
         <|> HDef  <$> (reserved "define"     *> defineP)
         <|> HMat  <$> (reserved "match"      *> matchP)
         <|> HDat  <$> (reserved "data"       *> dataDeclP)
+        <|> HNum  <$> (reserved "numeric"    *> numericDeclP)
+
+numericDeclP :: Parser ()
+numericDeclP = do
+  sym <- locUpperIdP
+  addNumTyCon (F.val sym)
 
 -------------------------------------------------------------------------------
 hCstrP :: Parser (H.Cstr H.Tag)
diff --git a/src/Language/Fixpoint/Horn/Types.hs b/src/Language/Fixpoint/Horn/Types.hs
--- a/src/Language/Fixpoint/Horn/Types.hs
+++ b/src/Language/Fixpoint/Horn/Types.hs
@@ -128,7 +128,7 @@
                    (_,so):xts -> F.mkQ "Auto" ((v, so) : xts) p junk
                    _          -> F.panic "impossible"
   where
-    xs         = L.delete v $ Misc.hashNub (F.syms p)
+    xs         = L.delete v $ Misc.setNub (F.syms p)
     junk       = F.dummyPos "mkQual"
 
 envSort :: F.SEnv F.Sort -> F.Symbol -> (F.Symbol, F.Sort)
diff --git a/src/Language/Fixpoint/Misc.hs b/src/Language/Fixpoint/Misc.hs
--- a/src/Language/Fixpoint/Misc.hs
+++ b/src/Language/Fixpoint/Misc.hs
@@ -19,6 +19,8 @@
 import qualified Data.HashMap.Strict              as M
 import qualified Data.List                        as L
 import qualified Data.HashSet                     as S
+import qualified Data.Map                         as Map
+import qualified Data.Set                         as Set
 import           Data.Tuple                       (swap)
 import           Data.Maybe
 import           Data.Array                       hiding (indices)
@@ -205,8 +207,8 @@
 allMap :: (Eq k, Hashable k) => (v -> Bool) -> M.HashMap k v -> Bool
 allMap p = L.foldl' (\a v -> a && p v) True
 
-hashNub :: (Eq k, Hashable k) => [k] -> [k]
-hashNub = M.keys . M.fromList . fmap (, ())
+setNub :: Ord k => [k] -> [k]
+setNub = Set.toList . Set.fromList
 
 sortNub :: (Ord a) => [a] -> [a]
 sortNub = nubOrd . L.sort
@@ -220,8 +222,8 @@
   | otherwise = x : nubOrd t
 nubOrd xs     = xs
 
-hashNubWith :: (Eq b, Hashable b) => (a -> b) -> [a] -> [a]
-hashNubWith f xs = M.elems $ M.fromList [ (f x, x) | x <- xs ]
+hashNubWith :: Ord b => (a -> b) -> [a] -> [a]
+hashNubWith f xs = Map.elems $ Map.fromList [ (f x, x) | x <- xs ]
 
 mFromList :: (Eq k, Hashable k) => [(k, v)] -> M.HashMap k v
 mFromList = M.fromList
diff --git a/src/Language/Fixpoint/Parse.hs b/src/Language/Fixpoint/Parse.hs
--- a/src/Language/Fixpoint/Parse.hs
+++ b/src/Language/Fixpoint/Parse.hs
@@ -52,7 +52,6 @@
   , refP        -- (Sorted) Refinements
   , refDefP     -- (Sorted) Refinements with default binder
   , refBindP    -- (Sorted) Refinements with configurable sub-parsers
-  , bvSortP     -- Bit-Vector Sort
   , defineP     -- function definition equations (PLE)
   , matchP      -- measure definition equations (PLE)
 
@@ -94,7 +93,7 @@
   , initPState, PState (..)
 
   , LayoutStack(..)
-  , Fixity(..), Assoc(..), addOperatorP
+  , Fixity(..), Assoc(..), addOperatorP, addNumTyCon
 
   -- * For testing
   , expr0P
@@ -120,7 +119,6 @@
 import           GHC.Generics                (Generic)
 
 import qualified Data.Char                   as Char
-import           Language.Fixpoint.Smt.Bitvector
 import           Language.Fixpoint.Types.Errors
 import qualified Language.Fixpoint.Misc      as Misc
 import           Language.Fixpoint.Smt.Types
@@ -207,6 +205,7 @@
                      , singList    :: Maybe (Expr -> Expr)
                      , supply      :: !Integer
                      , layoutStack :: LayoutStack
+                     , numTyCons   :: !(S.HashSet Symbol)
                      }
 
 -- | The layout stack tracks columns at which layout blocks
@@ -855,6 +854,10 @@
                     , fixityOps   = op:fixityOps s
                     }
 
+-- | Add a new numeric FTyCon (symbol) to the parsing state.
+addNumTyCon :: Symbol -> Parser ()
+addNumTyCon tc = modify $ \s -> s{ numTyCons = S.insert tc (numTyCons s) }
+
 -- | Parses any of the known infix operators.
 infixSymbolP :: Parser Symbol
 infixSymbolP = do
@@ -1000,7 +1003,6 @@
    =  parens sortP -- parenthesised sort, starts with "("
   <|> (reserved "func" >> funcSortP) -- function sort, starts with "func"
   <|> (fAppTC listFTyCon . pure <$> brackets sortP)
-  -- <|> bvSortP -- Andres: this looks unreachable, as it starts with "("
   <|> (fAppTC <$> fTyConP <*> appArgsP)
   <|> (fApp   <$> tvarP   <*> appArgsP)
 
@@ -1020,15 +1022,12 @@
   <|> (reserved "bool"    >> return boolFTyCon)
   <|> (reserved "num"     >> return numFTyCon)
   <|> (reserved "Str"     >> return strFTyCon)
-  <|> (symbolFTycon      <$> locUpperIdP)
+  <|> (mkFTycon          =<<  locUpperIdP)
 
--- | Bit-Vector Sort
-bvSortP :: Parser Sort
-bvSortP = mkSort <$> (bvSizeP "Size32" S32 <|> bvSizeP "Size64" S64)
-  where
-    bvSizeP ss s = do
-      parens (reserved "BitVec" >> reserved ss)
-      return s
+mkFTycon :: LocSymbol -> Parser FTycon
+mkFTycon locSym = do
+  nums  <- gets numTyCons
+  return (symbolNumInfoFTyCon locSym (val locSym `S.member` nums) False)
 
 
 --------------------------------------------------------------------------------
@@ -1101,8 +1100,14 @@
            , [InfixR (reservedOp "=>"   >> return PImp)]
            , [InfixR (reservedOp "==>"  >> return PImp)]
            , [InfixR (reservedOp "="    >> return PIff)]
-           , [InfixR (reservedOp "<=>"  >> return PIff)]]
+           , [InfixR (reservedOp "<=>"  >> return PIff)]
+           , [InfixR (reservedOp "!="   >> return pNotIff)]
+           , [InfixR (reservedOp "/="   >> return pNotIff)]
+           ]
 
+pNotIff :: Expr -> Expr -> Expr
+pNotIff x y = PNot (PIff x y)
+
 -- | Parses a relation predicate.
 --
 -- Binary relations connect expressions and predicates.
@@ -1453,6 +1458,7 @@
                            , fixityOps   = []
                            , supply      = 0
                            , layoutStack = Empty
+                           , numTyCons   = S.empty
                            }
 
 -- | Entry point for parsing, for testing.
diff --git a/src/Language/Fixpoint/Smt/Bitvector.hs b/src/Language/Fixpoint/Smt/Bitvector.hs
deleted file mode 100644
--- a/src/Language/Fixpoint/Smt/Bitvector.hs
+++ /dev/null
@@ -1,70 +0,0 @@
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveGeneric      #-}
-
-module Language.Fixpoint.Smt.Bitvector
-       ( -- * Constructor
-         Bv (..)
-
-         -- * Sizes
-       , BvSize (..)
-
-         -- * Operators
-       , BvOp (..)
-
-         -- * BitVector Sort Constructor
-       , mkSort
-
-         -- * BitVector Expression Constructor
-       , eOp
-
-         -- * BitVector Type Constructor
-       , bvTyCon
-
-       ) where
-
-import           Data.Generics           (Data)
-import qualified Data.Text               as T
-import           Data.Typeable           (Typeable)
-import           GHC.Generics            (Generic)
-import           Language.Fixpoint.Types.Names
-import           Language.Fixpoint.Types
-import           Data.List (foldl')
-
-data Bv     = Bv !BvSize !String
-
-data BvSize = S32   | S64
-              deriving (Eq, Ord, Show, Data, Typeable, Generic)
-
-data BvOp   = BvAnd | BvOr
-              deriving (Eq, Ord, Show, Data, Typeable, Generic)
-
--- | Construct the bitvector `Sort` from its `BvSize`
-mkSort :: BvSize -> Sort
-mkSort s = fApp (fTyconSort bvTyCon) [ fTyconSort (sizeTyCon s) ]
-
-bvTyCon :: FTycon
-bvTyCon = symbolFTycon $ dummyLoc bitVecName
-
-sizeTyCon    :: BvSize -> FTycon
-sizeTyCon    = symbolFTycon . dummyLoc . sizeName
-
-sizeName :: BvSize -> Symbol
-sizeName S32 = size32Name
-sizeName S64 = size64Name
-
--- | Construct an `Expr` using a raw string, e.g. (Bv S32 "#x02000000")
-instance Expression Bv where
-  expr (Bv sz v) = ECon $ L (T.pack v) (mkSort sz)
-
--- | Apply some bitvector operator to a list of arguments
-eOp :: BvOp -> [Expr] -> Expr
-eOp b es = foldl' EApp (EVar $ opName b) es
-
-opName :: BvOp -> Symbol
-opName BvAnd = bvAndName
-opName BvOr  = bvOrName
-
-
--- sizeSort     = (`FApp` [fObj $ dummyLoc $ symbol "obj"]) . sizeTC
--- s32TyCon     = symbolFTycon $ dummyLoc size32Name
--- s64TyCon     = symbolFTycon $ dummyLoc size64Name
diff --git a/src/Language/Fixpoint/Smt/Interface.hs b/src/Language/Fixpoint/Smt/Interface.hs
--- a/src/Language/Fixpoint/Smt/Interface.hs
+++ b/src/Language/Fixpoint/Smt/Interface.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE CPP                       #-}
 {-# LANGUAGE BangPatterns              #-}
 {-# LANGUAGE FlexibleInstances         #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
@@ -7,6 +6,7 @@
 {-# LANGUAGE UndecidableInstances      #-}
 {-# LANGUAGE ScopedTypeVariables       #-}
 {-# LANGUAGE PatternGuards             #-}
+{-# LANGUAGE DoAndIfThenElse           #-}
 
 {-# OPTIONS_GHC -Wno-name-shadowing #-}
 
@@ -18,23 +18,6 @@
 --   http://www.smt-lib.org/
 --   http://www.grammatech.com/resource/smt/SMTLIBTutorial.pdf
 
--- Note [Async SMT API]
---
--- The SMT solver is started in a separate process and liquid-fixpoint
--- communicates with it via pipes. This mechanism introduces some latency
--- since the queries need to reach the buffers in a separate process and
--- the OS has to switch contexts.
---
--- A remedy we currently try for this is to send multiple queries
--- together without waiting for the reply to each one, i.e. asynchronously.
--- We then collect the multiple answers after sending all of the queries.
---
--- The functions named @smt*Async@ implement this scheme.
---
--- An asynchronous thread is used to write the queries to prevent the
--- caller from blocking on IO, should the write buffer be full or should
--- an 'hFlush' call be necessary.
-
 module Language.Fixpoint.Smt.Interface (
 
     -- * Commands
@@ -55,7 +38,6 @@
 
     -- * Execute Queries
     , command
-    , smtExit
     , smtSetMbqi
 
     -- * Query API
@@ -70,12 +52,6 @@
     , smtBracket, smtBracketAt
     , smtDistinct
     , smtPush, smtPop
-    , smtAssertAsync
-    , smtCheckUnsatAsync
-    , readCheckUnsat
-    , smtBracketAsyncAt
-    , smtPushAsync
-    , smtPopAsync
 
     -- * Check Validity
     , checkValid
@@ -85,9 +61,6 @@
 
     ) where
 
-import           Control.Concurrent.Async (async, cancel)
-import           Control.Concurrent.STM
-  (TVar, atomically, modifyTVar, newTVarIO, readTVar, retry, writeTVar)
 import           Language.Fixpoint.Types.Config ( SMTSolver (..)
                                                 , Config
                                                 , solver
@@ -105,20 +78,22 @@
 import           Control.Applicative      ((<|>))
 import           Control.Monad
 import           Control.Exception
+import           Data.ByteString.Builder (Builder)
+import qualified Data.ByteString.Builder as BS
+import qualified Data.ByteString.Lazy as LBS
+import qualified Data.ByteString.Lazy.Char8 as Char8
 import           Data.Char
 import qualified Data.HashMap.Strict      as M
 import           Data.Maybe              (fromMaybe)
 import qualified Data.Text                as T
+import qualified Data.Text.Encoding       as TE
+import qualified Data.Text.IO
 -- import           Data.Text.Format
-import qualified Data.Text.IO             as TIO
-import qualified Data.Text.Lazy           as LT
 import qualified Data.Text.Lazy.IO        as LTIO
 import           System.Directory
 import           System.Console.CmdArgs.Verbosity
-import           System.Exit              hiding (die)
 import           System.FilePath
 import           System.IO
-import           System.Process
 import qualified Data.Attoparsec.Text     as A
 -- import qualified Data.HashMap.Strict      as M
 import           Data.Attoparsec.Internal.Types (Parser)
@@ -127,6 +102,10 @@
 import           Language.Fixpoint.Utils.Builder as Builder
 -- import qualified Language.Fixpoint.Types as F
 -- import           Language.Fixpoint.Types.PrettyPrint (tracepp)
+import qualified SMTLIB.Backends
+import qualified SMTLIB.Backends.Process as Process
+import qualified Language.Fixpoint.Conditional.Z3 as Conditional.Z3
+import Control.Concurrent.Async (async)
 
 {-
 runFile f
@@ -183,36 +162,37 @@
 {-# SCC command #-}
 command              :: Context -> Command -> IO Response
 --------------------------------------------------------------------------------
-command me !cmd       = say >> hear cmd
+command Ctx {..} !cmd       = do
+  -- whenLoud $ do LTIO.appendFile debugFile (s <> "\n")
+  --               LTIO.putStrLn ("CMD-RAW:" <> s <> ":CMD-RAW:DONE")
+  forM_ ctxLog $ \h -> do
+    BS.hPutBuilder h cmdBS
+    LBS.hPutStr h "\n"
+  case cmd of
+    CheckSat   -> commandRaw
+    GetValue _ -> commandRaw
+    _          -> SMTLIB.Backends.command_ ctxSolver cmdBS >> return Ok
   where
-    env               = ctxSymEnv me
-    say               = smtWrite me ({-# SCC "Command-runSmt2" #-} Builder.toLazyText (runSmt2 env cmd))
-    hear CheckSat     = smtRead me
-    hear (GetValue _) = smtRead me
-    hear _            = return Ok
-
-smtExit :: Context -> IO ()
-smtExit me = asyncCommand me Exit
+    commandRaw      = do
+      resp <- SMTLIB.Backends.command ctxSolver cmdBS
+      let respTxt =
+            TE.decodeUtf8With (const $ const $ Just ' ') $
+            LBS.toStrict resp
+      parse respTxt
+    cmdBS = {-# SCC "Command-runSmt2" #-} runSmt2 ctxSymEnv cmd
+    parse resp      = do
+      case A.parseOnly responseP resp of
+        Left e  -> Misc.errorstar $ "SMTREAD:" ++ e
+        Right r -> do
+          let textResponse = "; SMT Says: " <> T.pack (show r)
+          forM_ ctxLog $ \h ->
+            Data.Text.IO.hPutStrLn h textResponse
+          when ctxVerbose $
+            Data.Text.IO.putStrLn textResponse
+          return r
 
 smtSetMbqi :: Context -> IO ()
-smtSetMbqi me = asyncCommand me SetMbqi
-
-smtWrite :: Context -> Raw -> IO ()
-smtWrite me !s = smtWriteRaw me s
-
-smtRead :: Context -> IO Response
-smtRead me = {- SCC "smtRead" -} do
-  when (ctxVerbose me) $ LTIO.putStrLn "SMT READ"
-  ln  <- smtReadRaw me
-  res <- A.parseWith (smtReadRaw me) responseP ln
-  case A.eitherResult res of
-    Left e  -> Misc.errorstar $ "SMTREAD:" ++ e
-    Right r -> do
-      maybe (return ()) (\h -> LTIO.hPutStrLn h $ blt ("; SMT Says: " <> bShow r)) (ctxLog me)
-      when (ctxVerbose me) $ LTIO.putStrLn $ blt ("SMT Says: " <> bShow r)
-      return r
-
-
+smtSetMbqi me = interact' me SetMbqi
 
 type SmtParser a = Parser T.Text a
 
@@ -254,42 +234,21 @@
   = do v <- A.char '(' *> A.takeWhile1 (/=')') <* A.char ')'
        return $ "(" <> v <> ")"
 
--- | Writes a line of input for the SMT solver and to the log if there is one.
-smtWriteRaw :: Context -> Raw -> IO ()
-smtWriteRaw me !s = {- SCC "smtWriteRaw" -} do
-  -- whenLoud $ do LTIO.appendFile debugFile (s <> "\n")
-  --               LTIO.putStrLn ("CMD-RAW:" <> s <> ":CMD-RAW:DONE")
-  hPutStrLnNow (ctxIn me) s
-  maybe (return ()) (`LTIO.hPutStrLn` s) (ctxLog me)
-
--- | Reads a line of output from the SMT solver.
-smtReadRaw :: Context -> IO T.Text
-smtReadRaw me = do
-  eof <- hIsEOF (ctxOut me)
-  if eof then Misc.errorstar "SMT returned End of File" else
-    TIO.hGetLine (ctxOut me)
-{-# SCC smtReadRaw  #-}
-
-hPutStrLnNow :: Handle -> LT.Text -> IO ()
-hPutStrLnNow h !s = LTIO.hPutStrLn h s >> hFlush h
-{-# SCC hPutStrLnNow #-}
-
 --------------------------------------------------------------------------
 -- | SMT Context ---------------------------------------------------------
 --------------------------------------------------------------------------
 
 --------------------------------------------------------------------------
-makeContext   :: Config -> FilePath -> IO Context
+makeContext :: Config -> FilePath -> IO Context
 --------------------------------------------------------------------------
 makeContext cfg f
-  = do me   <- makeProcess cfg
-       pre  <- smtPreamble cfg (solver cfg) me
-       createDirectoryIfMissing True $ takeDirectory smtFile
+  = do createDirectoryIfMissing True $ takeDirectory smtFile
        hLog <- openFile smtFile WriteMode
-       hSetBuffering hLog $ BlockBuffering $ Just $ 1024*1024*64
-       let me' = me { ctxLog = Just hLog }
-       mapM_ (smtWrite me') pre
-       return me'
+       hSetBuffering hLog $ BlockBuffering $ Just $ 1024 * 1024 * 64
+       me   <- makeContext' cfg $ Just hLog
+       pre  <- smtPreamble cfg (solver cfg) me
+       mapM_ (SMTLIB.Backends.command_ (ctxSolver me)) pre
+       return me
     where
        smtFile = extFileName Smt2 f
 
@@ -303,75 +262,82 @@
 
 makeContextNoLog :: Config -> IO Context
 makeContextNoLog cfg
-  = do me  <- makeProcess cfg
+  = do me  <- makeContext' cfg Nothing
        pre <- smtPreamble cfg (solver cfg) me
-       mapM_ (smtWrite me) pre
+       mapM_ (SMTLIB.Backends.command_ (ctxSolver me)) pre
        return me
 
-makeProcess :: Config -> IO Context
-makeProcess cfg
-  = do (hIn, hOut, _ ,pid) <- runInteractiveCommand $ smtCmd (solver cfg)
+makeProcess
+  :: Maybe Handle
+  -> Process.Config
+  -> IO (SMTLIB.Backends.Backend, IO ())
+makeProcess ctxLog cfg
+  = do handle@Process.Handle {hMaybeErr = Just hErr, ..} <- Process.new cfg
+       case ctxLog of
+         Nothing -> return ()
+         Just hLog -> void $ async $ forever
+           (do err <- LTIO.hGetLine hErr
+               LTIO.hPutStrLn hLog $ "OOPS, SMT solver error:" <> err
+           ) `catch` \ SomeException {} -> return ()
+       let backend = Process.toBackend handle
+       hSetBuffering hOut $ BlockBuffering $ Just $ 1024 * 1024 * 64
+       hSetBuffering hIn $ BlockBuffering $ Just $ 1024 * 1024 * 64
+       return (backend, Process.close handle)
+
+makeContext' :: Config -> Maybe Handle -> IO Context
+makeContext' cfg ctxLog
+  = do (backend, closeIO) <- case solver cfg of
+         Z3      ->
+           {- "z3 -smt2 -in"                   -}
+           {- "z3 -smtc SOFT_TIMEOUT=1000 -in" -}
+           {- "z3 -smtc -in MBQI=false"        -}
+           makeProcess ctxLog $ Process.defaultConfig
+                             { Process.exe = "z3"
+                             , Process.args = ["-smt2", "-in"] }
+         Z3mem   -> Conditional.Z3.makeZ3
+         Mathsat -> makeProcess ctxLog $ Process.defaultConfig
+                             { Process.exe = "mathsat"
+                             , Process.args = ["-input=smt2"] }
+         Cvc4    -> makeProcess ctxLog $
+                      Process.defaultConfig
+                             { Process.exe = "cvc4"
+                             , Process.args = ["--incremental", "-L", "smtlib2"] }
+       solver <- SMTLIB.Backends.initSolver SMTLIB.Backends.Queuing backend
        loud <- isLoud
-       hSetBuffering hOut $ BlockBuffering $ Just $ 1024*1024*64
-       hSetBuffering hIn $ BlockBuffering $ Just $ 1024*1024*64
-       -- See Note [Async SMT API]
-       queueTVar <- newTVarIO mempty
-       writerAsync <- async $ forever $ do
-         t <- atomically $ do
-           builder <- readTVar queueTVar
-           let t = Builder.toLazyText builder
-           when (LT.null t) retry
-           writeTVar queueTVar mempty
-           return t
-         LTIO.hPutStr hIn t
-         hFlush hIn
-       return Ctx { ctxPid     = pid
-                  , ctxIn      = hIn
-                  , ctxOut     = hOut
-                  , ctxLog     = Nothing
+       return Ctx { ctxSolver  = solver
+                  , ctxClose   = closeIO
+                  , ctxLog     = ctxLog
                   , ctxVerbose = loud
                   , ctxSymEnv  = mempty
-                  , ctxAsync   = writerAsync
-                  , ctxTVar    = queueTVar
                   }
 
--- | Close file handles and wait for the solver process to terminate.
-cleanupContext :: Context -> IO ExitCode
-cleanupContext Ctx{..} = do
-  cancel ctxAsync
-  hCloseMe "ctxIn" ctxIn
-  hCloseMe "ctxOut"  ctxOut
+-- | Close file handles and release the solver backend's resources.
+cleanupContext :: Context -> IO ()
+cleanupContext Ctx {..} = do
   maybe (return ()) (hCloseMe "ctxLog") ctxLog
-  waitForProcess ctxPid
+  ctxClose
 
 hCloseMe :: String -> Handle -> IO ()
 hCloseMe msg h = hClose h `catch` (\(exn :: IOException) -> putStrLn $ "OOPS, hClose breaks: " ++ msg ++ show exn)
 
-{- "z3 -smt2 -in"                   -}
-{- "z3 -smtc SOFT_TIMEOUT=1000 -in" -}
-{- "z3 -smtc -in MBQI=false"        -}
-
-smtCmd         :: SMTSolver -> String --  T.Text
-smtCmd Z3      = "z3 -smt2 -in"
-smtCmd Mathsat = "mathsat -input=smt2"
-smtCmd Cvc4    = "cvc4 --incremental -L smtlib2"
-
-smtPreamble :: Config -> SMTSolver -> Context -> IO [LT.Text]
-smtPreamble cfg Z3 me
-  = do v <- getZ3Version me
-       checkValidStringFlag Z3 v cfg
-       return $ z3_options ++ makeMbqi cfg ++ makeTimeout cfg ++ Thy.preamble cfg Z3
-smtPreamble cfg s _
-  = checkValidStringFlag s [] cfg >> return (Thy.preamble cfg s)
+smtPreamble :: Config -> SMTSolver -> Context -> IO [Builder]
+smtPreamble cfg s me
+  | s == Z3 || s == Z3mem
+    = do v <- getZ3Version me
+         checkValidStringFlag Z3 v cfg
+         return $ z3_options ++ makeMbqi cfg ++ makeTimeout cfg ++ Thy.preamble cfg Z3
+  | otherwise
+    = checkValidStringFlag s [] cfg >> return (Thy.preamble cfg s)
 
 getZ3Version :: Context -> IO [Int]
 getZ3Version me
-  = do smtWrite me "(get-info :version)"
-       -- resp is like (:version "4.8.15")
-       resp <- smtReadRaw me
-       case T.splitOn "\"" resp of
-         _:vText:_ -> do
-           let parsedComponents = [ reads (T.unpack cText) | cText <- T.splitOn "." vText ]
+  = do -- resp is like (:version "4.8.15")
+       resp <- SMTLIB.Backends.command (ctxSolver me) "(get-info :version)"
+       case Char8.split '"' resp of
+         _:rText:_ -> do
+           -- strip off potential " - build hashcode ..." suffix
+           let vText = Char8.takeWhile (not . isSpace) rText
+           let parsedComponents = [ reads (Char8.unpack cText) | cText <- Char8.split '.' vText ]
            sequence
              [ case pComponent of
                  [(c, "")] -> return c
@@ -419,7 +385,7 @@
 deconSort :: Sort -> ([Sort], Sort)
 deconSort t = case functionSort t of
                 Just (_, ins, out) -> (ins, out)
-                Nothing            -> ([] , t  )
+                Nothing            -> ([], t)
 
 -- hack now this is used only for checking gradual condition.
 smtCheckSat :: Context -> Expr -> IO Bool
@@ -443,48 +409,7 @@
           e
 
 -----------------------------------------------------------------
--- Async calls to the smt
---
--- See Note [Async SMT API]
------------------------------------------------------------------
 
-asyncCommand :: Context -> Command -> IO ()
-asyncCommand me cmd = do
-  let env = ctxSymEnv me
-      cmdText = {-# SCC "asyncCommand-runSmt2" #-} Builder.toLazyText $ runSmt2 env cmd
-  asyncPutStrLn (ctxTVar me) cmdText
-  maybe (return ()) (`LTIO.hPutStrLn` cmdText) (ctxLog me)
-  where
-    asyncPutStrLn :: TVar Builder.Builder -> LT.Text -> IO ()
-    asyncPutStrLn tv t = atomically $
-      modifyTVar tv (`mappend` (Builder.fromLazyText t `mappend` Builder.fromString "\n"))
-
-smtAssertAsync :: Context -> Expr -> IO ()
-smtAssertAsync me p  = asyncCommand me $ Assert Nothing p
-
-smtCheckUnsatAsync :: Context -> IO ()
-smtCheckUnsatAsync me = asyncCommand me CheckSat
-
-smtBracketAsyncAt :: SrcSpan -> Context -> String -> IO a -> IO a
-smtBracketAsyncAt sp x y z = smtBracketAsync x y z `catch` dieAt sp
-
-smtBracketAsync :: Context -> String -> IO a -> IO a
-smtBracketAsync me _msg a   = do
-  smtPushAsync me
-  r <- a
-  smtPopAsync me
-  return r
-
-smtPushAsync, smtPopAsync   :: Context -> IO ()
-smtPushAsync me = asyncCommand me Push
-smtPopAsync me = asyncCommand me Pop
-
------------------------------------------------------------------
-
-{-# SCC readCheckUnsat #-}
-readCheckUnsat :: Context -> IO Bool
-readCheckUnsat me = respSat <$> smtRead me
-
 smtAssertAxiom :: Context -> Triggered Expr -> IO ()
 smtAssertAxiom me p  = interact' me (AssertAx p)
 
@@ -514,18 +439,18 @@
 interact' me cmd  = void $ command me cmd
 
 
-makeTimeout :: Config -> [LT.Text]
+makeTimeout :: Config -> [Builder]
 makeTimeout cfg
-  | Just i <- smtTimeout cfg = [ LT.pack ("\n(set-option :timeout " ++ show i ++ ")\n")]
+  | Just i <- smtTimeout cfg = [ "\n(set-option :timeout " <> fromString (show i) <> ")\n"]
   | otherwise                = [""]
 
 
-makeMbqi :: Config -> [LT.Text]
+makeMbqi :: Config -> [Builder]
 makeMbqi cfg
   | gradual cfg = [""]
   | otherwise   = ["\n(set-option :smt.mbqi false)"]
 
-z3_options :: [LT.Text]
+z3_options :: [Builder]
 z3_options
   = [ "(set-option :auto-config false)"
     , "(set-option :model true)" ]
diff --git a/src/Language/Fixpoint/Smt/Serialize.hs b/src/Language/Fixpoint/Smt/Serialize.hs
--- a/src/Language/Fixpoint/Smt/Serialize.hs
+++ b/src/Language/Fixpoint/Smt/Serialize.hs
@@ -15,6 +15,7 @@
 
 module Language.Fixpoint.Smt.Serialize (smt2SortMono) where
 
+import           Data.ByteString.Builder (Builder)
 import           Language.Fixpoint.SortCheck
 import           Language.Fixpoint.Types
 import qualified Language.Fixpoint.Types.Visitor as Vis
@@ -30,44 +31,44 @@
   smt2 env c@(sym, t) = -- build "({} {})" (smt2 env sym, smt2SortMono c env t)
                         parenSeqs [smt2 env sym, smt2SortMono c env t]
 
-smt2SortMono, smt2SortPoly :: (PPrint a) => a -> SymEnv -> Sort -> Builder.Builder
+smt2SortMono, smt2SortPoly :: (PPrint a) => a -> SymEnv -> Sort -> Builder
 smt2SortMono = smt2Sort False
 smt2SortPoly = smt2Sort True
 
-smt2Sort :: (PPrint a) => Bool -> a -> SymEnv -> Sort -> Builder.Builder
+smt2Sort :: (PPrint a) => Bool -> a -> SymEnv -> Sort -> Builder
 smt2Sort poly _ env t = smt2 env (Thy.sortSmtSort poly (seData env) t)
 
-smt2data :: SymEnv -> [DataDecl] -> Builder.Builder
+smt2data :: SymEnv -> [DataDecl] -> Builder
 smt2data env = smt2data' env . map padDataDecl
 
-smt2data' :: SymEnv -> [DataDecl] -> Builder.Builder
+smt2data' :: SymEnv -> [DataDecl] -> Builder
 smt2data' env ds = seqs [ parens $ smt2many (smt2dataname env <$> ds)
                          , parens $ smt2many (smt2datactors env <$> ds)
                          ]
 
 
-smt2dataname :: SymEnv -> DataDecl -> Builder.Builder
+smt2dataname :: SymEnv -> DataDecl -> Builder
 smt2dataname env (DDecl tc as _) = parenSeqs [name, n]
   where
     name  = smt2 env (symbol tc)
     n     = smt2 env as
 
 
-smt2datactors :: SymEnv -> DataDecl -> Builder.Builder
+smt2datactors :: SymEnv -> DataDecl -> Builder
 smt2datactors env (DDecl _ as cs) = parenSeqs ["par", parens tvars, parens ds]
   where
     tvars        = smt2many (smt2TV <$> [0..(as-1)])
     smt2TV       = smt2 env . SVar
     ds           = smt2many (smt2ctor env as <$> cs)
 
-smt2ctor :: SymEnv -> Int -> DataCtor -> Builder.Builder
+smt2ctor :: SymEnv -> Int -> DataCtor -> Builder
 smt2ctor env _  (DCtor c [])  = smt2 env c
 smt2ctor env as (DCtor c fs)  = parenSeqs [smt2 env c, fields]
 
   where
     fields                 = smt2many (smt2field env as <$> fs)
 
-smt2field :: SymEnv -> Int -> DataField -> Builder.Builder
+smt2field :: SymEnv -> Int -> DataField -> Builder
 smt2field env as d@(DField x t) = parenSeqs [smt2 env x, smt2SortPoly d env $ mkPoly as t]
 
 -- | SMTLIB/Z3 don't like "unused" type variables; they get pruned away and
@@ -112,7 +113,7 @@
 instance SMTLIB2 Constant where
   smt2 _ (I n)   = bShow n
   smt2 _ (R d)   = bFloat d
-  smt2 _ (L t _) = lbb t
+  smt2 _ (L t _) = fromText t
 
 instance SMTLIB2 Bop where
   smt2 _ Plus   = "+"
@@ -165,24 +166,24 @@
 -- | smt2Cast uses the 'as x T' pattern needed for polymorphic ADT constructors
 --   like Nil, see `tests/pos/adt_list_1.fq`
 
-smt2Cast :: SymEnv -> Expr -> Sort -> Builder.Builder
+smt2Cast :: SymEnv -> Expr -> Sort -> Builder
 smt2Cast env (EVar x) t = smt2Var env x t
 smt2Cast env e        _ = smt2    env e
 
-smt2Var :: SymEnv -> Symbol -> Sort -> Builder.Builder
+smt2Var :: SymEnv -> Symbol -> Sort -> Builder
 smt2Var env x t
   | isLamArgSymbol x            = smtLamArg env x t
   | Just s <- symEnvSort x env
   , isPolyInst s t              = smt2VarAs env x t
   | otherwise                   = smt2 env x
 
-smtLamArg :: SymEnv -> Symbol -> Sort -> Builder.Builder
+smtLamArg :: SymEnv -> Symbol -> Sort -> Builder
 smtLamArg env x t = Builder.fromText $ symbolAtName x env () (FFunc t FInt)
 
-smt2VarAs :: SymEnv -> Symbol -> Sort -> Builder.Builder
+smt2VarAs :: SymEnv -> Symbol -> Sort -> Builder
 smt2VarAs env x t = parenSeqs ["as", smt2 env x, smt2SortMono x env t]
 
-smt2Lam :: SymEnv -> (Symbol, Sort) -> Expr -> Builder.Builder
+smt2Lam :: SymEnv -> (Symbol, Sort) -> Expr -> Builder
 smt2Lam env (x, xT) (ECst e eT) = parenSeqs [Builder.fromText lambda, x', smt2 env e]
   where
     x'                          = smtLamArg env x xT
@@ -191,7 +192,7 @@
 smt2Lam _ _ e
   = panic ("smtlib2: Cannot serialize unsorted lambda: " ++ showpp e)
 
-smt2App :: SymEnv -> Expr -> Builder.Builder
+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]]
@@ -203,15 +204,13 @@
   where
     (f, es)   = splitEApp' e
 
-smt2Coerc :: SymEnv -> Sort -> Sort -> Expr -> Builder.Builder
+smt2Coerc :: SymEnv -> Sort -> Sort -> Expr -> Builder
 smt2Coerc env t1 t2 e
-  | t1' == t2'  = smt2 env e
+  | t1 == t2  = smt2 env e
   | otherwise = parenSeqs [Builder.fromText coerceFn , smt2 env e]
   where
     coerceFn  = symbolAtName coerceName env (ECoerc t1 t2 e) t
     t         = FFunc t1 t2
-    t1'       = smt2SortMono e env t1
-    t2'       = smt2SortMono e env t2
 
 splitEApp' :: Expr -> (Expr, [Expr])
 splitEApp'            = go []
@@ -220,12 +219,12 @@
   --   go acc (ECst e _) = go acc e
     go acc e          = (e, acc)
 
-mkRel :: SymEnv -> Brel -> Expr -> Expr -> Builder.Builder
+mkRel :: SymEnv -> Brel -> Expr -> Expr -> Builder
 mkRel env Ne  e1 e2 = mkNe env e1 e2
 mkRel env Une e1 e2 = mkNe env e1 e2
 mkRel env r   e1 e2 = parenSeqs [smt2 env r, smt2 env e1, smt2 env e2]
 
-mkNe :: SymEnv -> Expr -> Expr -> Builder.Builder
+mkNe :: SymEnv -> Expr -> Expr -> Builder
 mkNe env e1 e2      = key "not" (parenSeqs ["=",  smt2 env e1, smt2 env e2])
 
 instance SMTLIB2 Command where
@@ -258,13 +257,13 @@
   smt2 env (TR _ e)               = smt2 env e
 
 {-# INLINE smtTr #-}
-smtTr :: SymEnv -> Builder.Builder -> [(Symbol, Sort)] -> Expr -> Triggered Expr -> Builder.Builder
+smtTr :: SymEnv -> Builder -> [(Symbol, Sort)] -> Expr -> Triggered Expr -> Builder
 smtTr env q bs p t = key q (parens (smt2s env bs) <+> key "!" (smt2 env p <+> ":pattern" <> parens (smt2s env (makeTriggers t))))
 
 {-# INLINE smt2s #-}
-smt2s    :: SMTLIB2 a => SymEnv -> [a] -> Builder.Builder
+smt2s    :: SMTLIB2 a => SymEnv -> [a] -> Builder
 smt2s env as = smt2many (smt2 env <$> as)
 
 {-# INLINE smt2many #-}
-smt2many :: [Builder.Builder] -> Builder.Builder
+smt2many :: [Builder] -> Builder
 smt2many = seqs
diff --git a/src/Language/Fixpoint/Smt/Theories.hs b/src/Language/Fixpoint/Smt/Theories.hs
--- a/src/Language/Fixpoint/Smt/Theories.hs
+++ b/src/Language/Fixpoint/Smt/Theories.hs
@@ -42,13 +42,13 @@
      ) where
 
 import           Prelude hiding (map)
+import           Data.ByteString.Builder (Builder)
 import           Language.Fixpoint.Types.Sorts
 import           Language.Fixpoint.Types.Config
 import           Language.Fixpoint.Types
 import           Language.Fixpoint.Smt.Types
 -- import qualified Data.HashMap.Strict      as M
 import           Data.Maybe (catMaybes)
-import qualified Data.Text.Lazy           as T
 -- import           Data.Text.Format
 import qualified Data.Text
 import           Data.String                 (IsString(..))
@@ -92,7 +92,61 @@
 mshift = "smt_map_shift"
 mToSet = "smt_map_to_set"
 
+---- Size changes
+bvConcatName, bvExtractName, bvRepeatName, bvZeroExtName, bvSignExtName :: Symbol
+bvConcatName   = "concat"
+bvExtractName  = "extract"
+bvRepeatName   = "repeat"
+bvZeroExtName  = "zero_extend"
+bvSignExtName  = "sign_extend"
 
+-- Unary Logic
+bvNotName, bvNegName :: Symbol
+bvNotName = "bvnot"
+bvNegName = "bvneg"
+
+-- Binary Logic
+bvAndName, bvNandName, bvOrName, bvNorName, bvXorName, bvXnorName :: Symbol
+bvAndName  = "bvand"
+bvNandName = "bvnand"
+bvOrName   = "bvor"
+bvNorName  = "bvnor"
+bvXorName  = "bvxor"
+bvXnorName = "bvxnor"
+
+-- Shifts
+bvShlName, bvLShrName, bvAShrName, bvLRotName, bvRRotName :: Symbol
+bvShlName  = "bvshl"
+bvLShrName = "bvlshr"
+bvAShrName = "bvashr"
+bvLRotName = "rotate_left"
+bvRRotName = "rotate_right"
+
+-- Arithmetic
+bvAddName, bvSubName, bvMulName, bvUDivName :: Symbol
+bvURemName, bvSDivName, bvSRemName, bvSModName :: Symbol
+bvAddName  = "bvadd"
+bvSubName  = "bvsub"
+bvMulName  = "bvmul"
+bvUDivName = "bvudiv"
+bvURemName = "bvurem"
+bvSDivName = "bvsdiv"
+bvSRemName = "bvsrem"
+bvSModName = "bvsmod"
+
+-- Comparisons
+bvCompName, bvULtName, bvULeName, bvUGtName, bvUGeName :: Symbol
+bvSLtName, bvSLeName, bvSGtName, bvSGeName :: Symbol
+bvCompName = "bvcomp"
+bvULtName  = "bvult"
+bvULeName  = "bvule"
+bvUGtName  = "bvugt"
+bvUGeName  = "bvuge"
+bvSLtName  = "bvslt"
+bvSLeName  = "bvsle"
+bvSGtName  = "bvsgt"
+bvSGeName  = "bvsge"
+
 setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup :: Symbol
 setDif, setSng :: Symbol
 setEmpty = "Set_empty"
@@ -169,199 +223,196 @@
 string :: Raw
 string = strConName
 
-bFun :: Raw -> [(Builder, Builder)] -> Builder -> Builder -> T.Text
-bFun name xts out body = blt $ key "define-fun" (seqs [bb name, args, out, body])
+bFun :: Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
+bFun name xts out body = key "define-fun" (seqs [fromText name, args, out, body])
   where
     args = parenSeqs [parens (x <+> t) | (x, t) <- xts]
 
-bFun' :: Raw -> [Builder] -> Builder -> T.Text
-bFun' name ts out = blt $ key "declare-fun" (seqs [bb name, args, out])
+bFun' :: Raw -> [Builder] -> Builder -> Builder
+bFun' name ts out = key "declare-fun" (seqs [fromText name, args, out])
   where
     args = parenSeqs ts
 
-bSort :: Raw -> Builder -> T.Text
-bSort name def = blt $ key "define-sort" (bb name <+> "()" <+> def)
+bSort :: Raw -> Builder -> Builder
+bSort name def = key "define-sort" (fromText name <+> "()" <+> def)
 
-z3Preamble :: Config -> [T.Text]
+z3Preamble :: Config -> [Builder]
 z3Preamble u
   = stringPreamble u ++
     [ bSort elt
         "Int"
     , bSort set
-        (key2 "Array" (bb elt) "Bool")
+        (key2 "Array" (fromText elt) "Bool")
     , bFun emp
         []
-        (bb set)
-        (parens (key "as const" (bb set) <+> "false"))
+        (fromText set)
+        (parens (key "as const" (fromText set) <+> "false"))
     , bFun sng
-        [("x", bb elt)]
-        (bb set)
-        (key3 "store" (parens (key "as const" (bb set) <+> "false")) "x" "true")
+        [("x", fromText elt)]
+        (fromText set)
+        (key3 "store" (parens (key "as const" (fromText set) <+> "false")) "x" "true")
     , bFun mem
-        [("x", bb elt), ("s", bb set)]
+        [("x", fromText elt), ("s", fromText set)]
         "Bool"
         "(select s x)"
     , bFun add
-        [("s", bb set), ("x", bb elt)]
-        (bb set)
+        [("s", fromText set), ("x", fromText elt)]
+        (fromText set)
         "(store s x true)"
     , bFun cup
-        [("s1", bb set), ("s2", bb set)]
-        (bb set)
+        [("s1", fromText set), ("s2", fromText set)]
+        (fromText set)
         "((_ map or) s1 s2)"
     , bFun cap
-        [("s1", bb set), ("s2", bb set)]
-        (bb set)
+        [("s1", fromText set), ("s2", fromText set)]
+        (fromText set)
         "((_ map and) s1 s2)"
     , bFun com
-        [("s", bb set)]
-        (bb set)
+        [("s", fromText set)]
+        (fromText set)
         "((_ map not) s)"
     , bFun dif
-        [("s1", bb set), ("s2", bb set)]
-        (bb set)
-        (key2 (bb cap) "s1" (key (bb com) "s2"))
+        [("s1", fromText set), ("s2", fromText set)]
+        (fromText set)
+        (key2 (fromText cap) "s1" (key (fromText com) "s2"))
     , bFun sub
-        [("s1", bb set), ("s2", bb set)]
+        [("s1", fromText set), ("s2", fromText set)]
         "Bool"
-        (key2 "=" (bb emp) (key2 (bb dif) "s1" "s2"))
+        (key2 "=" (fromText emp) (key2 (fromText dif) "s1" "s2"))
 
     -- Maps
     , bSort map
-        (key2 "Array" (bb elt) (bb elt))
+        (key2 "Array" (fromText elt) (fromText elt))
     , bFun sel
-        [("m", bb map), ("k", bb elt)]
-        (bb elt)
+        [("m", fromText map), ("k", fromText elt)]
+        (fromText elt)
         "(select m k)"
     , bFun sto
-        [("m", bb map), ("k", bb elt), ("v", bb elt)]
-        (bb map)
+        [("m", fromText map), ("k", fromText elt), ("v", fromText elt)]
+        (fromText map)
         "(store m k v)"
     , bFun mcup
-        [("m1", bb map), ("m2", bb map)]
-        (bb map)
-        (key2 (key "_ map" (key2 "+" (parens (bb elt <+> bb elt)) (bb elt))) "m1" "m2")
+        [("m1", fromText map), ("m2", fromText map)]
+        (fromText map)
+        (key2 (key "_ map" (key2 "+" (parens (fromText elt <+> fromText elt)) (fromText elt))) "m1" "m2")
     , bFun mprj -- See [Interaction Between Map and Set]
-        [("s", bb set), ("m", bb map)]
-        (bb map)
+        [("s", fromText set), ("m", fromText map)]
+        (fromText map)
         (key3
           (key "_ map"
             (key2 "ite"
-              (parens ("Bool" <+> bb elt <+> bb elt))
-              (bb elt)
+              (parens ("Bool" <+> fromText elt <+> fromText elt))
+              (fromText elt)
             )
           )
           "s"
           "m"
-          (parens (key "as const" (key2 "Array" (bb elt) (bb elt)) <+> "0"))
+          (parens (key "as const" (key2 "Array" (fromText elt) (fromText elt)) <+> "0"))
         )
     , bFun mToSet -- See [Interaction Between Map and Set]
-        [("m", bb map)]
-        (bb set)
+        [("m", fromText map)]
+        (fromText set)
         (key2
           (key "_ map"
             (key2 ">"
-              (parens (bb elt <+> bb elt))
+              (parens (fromText elt <+> fromText elt))
               "Bool"
             )
           )
           "m"
-          (parens (key "as const" (key2 "Array" (bb elt) (bb elt)) <+> "0"))
+          (parens (key "as const" (key2 "Array" (fromText elt) (fromText elt)) <+> "0"))
         )
     , bFun mmax -- See [Map max and min]
-        [("m1", bb map),("m2", bb map)]
-        (bb map)
+        [("m1", fromText map),("m2", fromText map)]
+        (fromText map)
         "(lambda ((i Int)) (ite (> (select m1 i) (select m2 i)) (select m1 i) (select m2 i)))"
     , bFun mmin -- See [Map max and min]
-        [("m1", bb map),("m2", bb map)]
-        (bb map)
+        [("m1", fromText map),("m2", fromText map)]
+        (fromText map)
         "(lambda ((i Int)) (ite (< (select m1 i) (select m2 i)) (select m1 i) (select m2 i)))"
     , bFun mshift -- See [Map key shift]
-        [("n", "Int"),("m", bb map)]
-        (bb map)
+        [("n", "Int"),("m", fromText map)]
+        (fromText map)
         "(lambda ((i Int)) (select m (- i n)))"
     , bFun mdef
-        [("v", bb elt)]
-        (bb map)
-        (key (key "as const" (parens (bb map))) "v")
+        [("v", fromText elt)]
+        (fromText map)
+        (key (key "as const" (parens (fromText map))) "v")
     , bFun boolToIntName
         [("b", "Bool")]
         "Int"
         "(ite b 1 0)"
 
-    , uifDef u (symbolLText mulFuncName) "*"
-    , uifDef u (symbolLText divFuncName) "div"
+    , uifDef u (symbolText mulFuncName) "*"
+    , uifDef u (symbolText divFuncName) "div"
     ]
 
-symbolLText :: Symbol -> T.Text
-symbolLText = T.fromStrict . symbolText
-
 -- RJ: Am changing this to `Int` not `Real` as (1) we usually want `Int` and
 -- (2) have very different semantics. TODO: proper overloading, post genEApp
-uifDef :: Config -> T.Text -> T.Text -> T.Text
+uifDef :: Config -> Data.Text.Text -> Data.Text.Text -> Builder
 uifDef cfg f op
   | linear cfg || Z3 /= solver cfg
   = bFun' f ["Int", "Int"] "Int"
   | otherwise
-  = bFun f [("x", "Int"), ("y", "Int")] "Int" (key2 (bb op) "x" "y")
+  = bFun f [("x", "Int"), ("y", "Int")] "Int" (key2 (fromText op) "x" "y")
 
-cvc4Preamble :: Config -> [T.Text]
+cvc4Preamble :: Config -> [Builder]
 cvc4Preamble z
   = [        "(set-logic ALL_SUPPORTED)"]
   ++ commonPreamble z
   ++ cvc4MapPreamble z
 
-commonPreamble :: Config -> [T.Text]
+commonPreamble :: Config -> [Builder]
 commonPreamble _ --TODO use uif flag u (see z3Preamble)
   = [ bSort elt    "Int"
     , bSort set    "Int"
     , bSort string "Int"
-    , bFun' emp []               (bb set)
-    , bFun' sng [bb elt]         (bb set)
-    , bFun' add [bb set, bb elt] (bb set)
-    , bFun' cup [bb set, bb set] (bb set)
-    , bFun' cap [bb set, bb set] (bb set)
-    , bFun' dif [bb set, bb set] (bb set)
-    , bFun' sub [bb set, bb set] "Bool"
-    , bFun' mem [bb elt, bb set] "Bool"
+    , bFun' emp []               (fromText set)
+    , bFun' sng [fromText elt]         (fromText set)
+    , bFun' add [fromText set, fromText elt] (fromText set)
+    , bFun' cup [fromText set, fromText set] (fromText set)
+    , bFun' cap [fromText set, fromText set] (fromText set)
+    , bFun' dif [fromText set, fromText set] (fromText set)
+    , bFun' sub [fromText set, fromText set] "Bool"
+    , bFun' mem [fromText elt, fromText set] "Bool"
     , bFun boolToIntName [("b", "Bool")] "Int" "(ite b 1 0)"
     ]
 
-cvc4MapPreamble :: Config -> [T.Text]
+cvc4MapPreamble :: Config -> [Builder]
 cvc4MapPreamble _ =
-    [ bSort map    (key2 "Array" (bb elt) (bb elt))
-    , bFun sel [("m", bb map), ("k", bb elt)]                (bb elt) "(select m k)"
-    , bFun sto [("m", bb map), ("k", bb elt), ("v", bb elt)] (bb map) "(store m k v)"
+    [ bSort map    (key2 "Array" (fromText elt) (fromText elt))
+    , bFun sel [("m", fromText map), ("k", fromText elt)]                (fromText elt) "(select m k)"
+    , bFun sto [("m", fromText map), ("k", fromText elt), ("v", fromText elt)] (fromText map) "(store m k v)"
     ]
 
-smtlibPreamble :: Config -> [T.Text]
+smtlibPreamble :: Config -> [Builder]
 smtlibPreamble z --TODO use uif flag u (see z3Preamble)
   = commonPreamble z
  ++ [ bSort map "Int"
-    , bFun' sel [bb map, bb elt] (bb elt)
-    , bFun' sto [bb map, bb elt, bb elt] (bb map)
+    , bFun' sel [fromText map, fromText elt] (fromText elt)
+    , bFun' sto [fromText map, fromText elt, fromText elt] (fromText map)
     ]
 
-stringPreamble :: Config -> [T.Text]
+stringPreamble :: Config -> [Builder]
 stringPreamble cfg | stringTheory cfg
   = [ bSort string "String"
-    , bFun strLen [("s", bb string)] "Int" (key (bb z3strlen) "s")
-    , bFun strSubstr [("s", bb string), ("i", "Int"), ("j", "Int")] (bb string) (key (bb z3strsubstr) "s i j")
-    , bFun strConcat [("x", bb string), ("y", bb string)] (bb string) (key (bb z3strconcat) "x y")
+    , bFun strLen [("s", fromText string)] "Int" (key (fromText z3strlen) "s")
+    , bFun strSubstr [("s", fromText string), ("i", "Int"), ("j", "Int")] (fromText string) (key (fromText z3strsubstr) "s i j")
+    , bFun strConcat [("x", fromText string), ("y", fromText string)] (fromText string) (key (fromText z3strconcat) "x y")
     ]
 
 stringPreamble _
   = [ bSort string "Int"
-    , bFun' strLen [bb string] "Int"
-    , bFun' strSubstr [bb string, "Int", "Int"] (bb string)
-    , bFun' strConcat [bb string, bb string] (bb string)
+    , bFun' strLen [fromText string] "Int"
+    , bFun' strSubstr [fromText string, "Int", "Int"] (fromText string)
+    , bFun' strConcat [fromText string, fromText string] (fromText string)
     ]
 
 --------------------------------------------------------------------------------
 -- | Exported API --------------------------------------------------------------
 --------------------------------------------------------------------------------
 smt2Symbol :: SymEnv -> Symbol -> Maybe Builder
-smt2Symbol env x = fromLazyText . tsRaw <$> symEnvTheory x env
+smt2Symbol env x = fromText . tsRaw <$> symEnvTheory x env
 
 instance SMTLIB2 SmtSort where
   smt2 _ = smt2SmtSort
@@ -370,9 +421,9 @@
 smt2SmtSort SInt         = "Int"
 smt2SmtSort SReal        = "Real"
 smt2SmtSort SBool        = "Bool"
-smt2SmtSort SString      = bb string
-smt2SmtSort SSet         = bb set
-smt2SmtSort SMap         = bb map
+smt2SmtSort SString      = fromText string
+smt2SmtSort SSet         = fromText set
+smt2SmtSort SMap         = fromText map
 smt2SmtSort (SBitVec n)  = key "_ BitVec" (bShow n)
 smt2SmtSort (SVar n)     = "T" <> bShow n
 smt2SmtSort (SData c []) = symbolBuilder c
@@ -388,9 +439,9 @@
 smt2App :: VarAs -> SymEnv -> Expr -> [Builder] -> Maybe Builder
 --------------------------------------------------------------------------------
 smt2App _ _ (dropECst -> EVar f) [d]
-  | f == setEmpty = Just (bb emp)
-  | f == setEmp   = Just (key2 "=" (bb emp) d)
-  | f == setSng   = Just (key (bb sng) d) -- Just (key2 (bb add) (bb emp) d)
+  | f == setEmpty = Just (fromText emp)
+  | f == setEmp   = Just (key2 "=" (fromText emp) d)
+  | f == setSng   = Just (key (fromText sng) d) -- Just (key2 (bb add) (bb emp) d)
 
 smt2App k env f (d:ds)
   | Just fb <- smt2AppArg k env f
@@ -403,7 +454,7 @@
   | Just fThy <- symEnvTheory f env
   = Just $ if isPolyCtor fThy t
             then k env f (ffuncOut t)
-            else bb (tsRaw fThy)
+            else fromText (tsRaw fThy)
 
 smt2AppArg _ _ _
   = Nothing
@@ -434,7 +485,7 @@
   Just (_, ts) -> Just (length ts - 1)
   Nothing      -> Nothing
 
-preamble :: Config -> SMTSolver -> [T.Text]
+preamble :: Config -> SMTSolver -> [Builder]
 preamble u Z3   = z3Preamble u
 preamble u Cvc4 = cvc4Preamble u
 preamble u _    = smtlibPreamble u
@@ -467,6 +518,7 @@
   , interpSym setDif   dif   setBopSort
   , interpSym setSub   sub   setCmpSort
   , interpSym setCom   com   setCmpSort
+
   , interpSym mapSel   sel   mapSelSort
   , interpSym mapSto   sto   mapStoSort
   , interpSym mapCup   mcup  mapCupSort
@@ -476,21 +528,80 @@
   , interpSym mapPrj   mprj  mapPrjSort
   , interpSym mapShift mshift mapShiftSort
   , interpSym mapToSet mToSet mapToSetSort
-  , interpSym bvOrName "bvor"   bvBopSort
-  , interpSym bvAndName "bvand" bvBopSort
+  -- , interpSym bvOrName  "bvor"  bvBopSort
+  -- , interpSym bvAndName "bvand" bvBopSort
+  -- , interpSym bvAddName "bvadd" bvBopSort
+  -- , interpSym bvSubName "bvsub" bvBopSort
+
   , interpSym strLen    strLen    strLenSort
   , interpSym strSubstr strSubstr substrSort
   , interpSym strConcat strConcat concatstrSort
   , interpSym boolInt   boolInt   (FFunc boolSort intSort)
+
+  -- Function mappings for indexed identifier functions
+  , interpSym' "_" iiSort
+  , interpSym "app" "" appSort
+
+  , interpSym' bvConcatName bvConcatSort
+  , interpSym' bvExtractName (FFunc FInt bvExtendSort)
+  , interpBvExt bvRepeatName
+  , interpBvExt bvZeroExtName
+  , interpBvExt bvSignExtName
+
+  , interpBvUop bvNotName
+  , interpBvUop bvNegName
+
+  , interpBvBop bvAndName
+  , interpBvBop bvNandName
+  , interpBvBop bvOrName
+  , interpBvBop bvNorName
+  , interpBvBop bvXorName
+  , interpBvBop bvXnorName
+
+  , interpBvBop bvShlName
+  , interpBvBop bvLShrName
+  , interpBvBop bvAShrName
+  , interpBvRot bvLRotName
+  , interpBvRot bvRRotName
+
+  , interpBvBop bvAddName
+  , interpBvBop bvSubName
+  , interpBvBop bvMulName
+  , interpBvBop bvUDivName
+  , interpBvBop bvURemName
+  , interpBvBop bvSDivName
+  , interpBvBop bvSRemName
+  , interpBvBop bvSModName
+
+  , interpSym' bvCompName bvEqSort
+  , interpBvCmp bvULtName
+  , interpBvCmp bvULeName
+  , interpBvCmp bvUGtName
+  , interpBvCmp bvUGeName
+  , interpBvCmp bvSLtName
+  , interpBvCmp bvSLeName
+  , interpBvCmp bvSGtName
+  , interpBvCmp bvSGeName
+
+  , interpSym intbv32Name "(_ int2bv 32)"   (FFunc intSort bv32)
+  , interpSym intbv64Name "(_ int2bv 64)"   (FFunc intSort bv64)
+  , interpSym bv32intName  "(_ bv2int 32)"  (FFunc bv32    intSort)
+  , interpSym bv64intName   "(_ bv2int 64)" (FFunc bv64    intSort)
+
   ]
   where
+    -- (sizedBitVecSort "Size1")
+    bv32       = sizedBitVecSort "Size32"
+    bv64       = sizedBitVecSort "Size64"
     boolInt    = boolToIntName
     setAddSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (FVar 0)           (setSort $ FVar 0)
     setBopSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) (setSort $ FVar 0)
     setMemSort = FAbs 0 $ FFunc (FVar 0) $ FFunc (setSort $ FVar 0) boolSort
     setCmpSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) boolSort
+    -- select :: forall i a. Map i a -> i -> a
     mapSelSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1))
                                  $ FFunc (FVar 0) (FVar 1)
+    -- cup :: forall i. Map i Int -> Map i Int -> Map i Int
     mapCupSort = FAbs 0          $ FFunc (mapSort (FVar 0) intSort)
                                  $ FFunc (mapSort (FVar 0) intSort)
                                          (mapSort (FVar 0) intSort)
@@ -503,6 +614,7 @@
                                  $ FFunc (mapSort intSort (FVar 0))
                                          (mapSort intSort (FVar 0))
     mapToSetSort = FAbs 0        $ FFunc (mapSort (FVar 0) intSort) (setSort (FVar 0))
+    -- store :: forall i a. Map i a -> i -> a -> Map i a
     mapStoSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1))
                                  $ FFunc (FVar 0)
                                  $ FFunc (FVar 1)
@@ -510,8 +622,83 @@
     mapDefSort = FAbs 0 $ FAbs 1 $ FFunc (FVar 1)
                                          (mapSort (FVar 0) (FVar 1))
 
-    bvBopSort  = FFunc bitVecSort $ FFunc bitVecSort bitVecSort
 
+interpBvUop :: Symbol -> (Symbol, TheorySymbol)
+interpBvUop name = interpSym' name bvUopSort
+interpBvBop :: Symbol -> (Symbol, TheorySymbol)
+interpBvBop name = interpSym' name bvBopSort
+interpBvCmp :: Symbol -> (Symbol, TheorySymbol)
+interpBvCmp name = interpSym' name bvCmpSort
+interpBvExt :: Symbol -> (Symbol, TheorySymbol)
+interpBvExt name = interpSym' name bvExtendSort
+interpBvRot :: Symbol -> (Symbol, TheorySymbol)
+interpBvRot name = interpSym' name bvRotSort
+
+interpSym' :: Symbol -> Sort -> (Symbol, TheorySymbol)
+interpSym' name = interpSym name (Data.Text.pack $ symbolString name)
+
+-- Indexed Identifier sort.
+-- Together with 'app', this allows one to write indexed identifier
+-- functions (smtlib2 specific functions). (e.g. ((_ sign_extend 1) bv))
+--
+-- The idea here is that 'app' is elaborated to the empty string,
+-- and '_' does the typelit application as it does in smtlib2.
+--
+-- Then if we write, (app (_ sign_extend 1) bv), LF will elaborate
+-- it as ( (_ sign_extend 1) bv). Fitting the smtlib2 format exactly!
+--
+-- One thing to note, is that any indexed identifier function (like
+-- sign_extend) has to have no FAbs in it. Otherwise, they will be
+-- elaborated like e.g. ( (_ (as sign_extend Int) 1) bv), which is wrong!
+--
+-- _ :: forall a b c. (a -> b -> c) -> a -> (b -> c)
+iiSort :: Sort
+iiSort = FAbs 0 $ FAbs 1 $ FAbs 2 $ FFunc
+               (FFunc (FVar 0) $ FFunc (FVar 1) (FVar 2))
+               (FFunc (FVar 0) $ FFunc (FVar 1) (FVar 2))
+
+-- Simple application, used for indexed identifier function, check '_'.
+--
+-- app :: forall a b. (a -> b) -> a -> b
+appSort :: Sort
+appSort = FAbs 0 $ FAbs 1 $ FFunc
+                (FFunc (FVar 0) (FVar 1))
+                (FFunc (FVar 0) (FVar 1))
+
+-- Indexed identifier operation, purposely didn't place FAbs!
+--
+-- extend :: Int -> BitVec a -> BitVec b
+bvExtendSort :: Sort
+bvExtendSort  = FFunc FInt $ FFunc (bitVecSort 1) (bitVecSort 2)
+
+-- Indexed identifier operation, purposely didn't place FAbs!
+--
+-- rot :: Int -> BitVec a -> BitVec a
+bvRotSort :: Sort
+bvRotSort  = FFunc FInt $ FFunc (bitVecSort 0) (bitVecSort 0)
+
+-- uOp :: forall a. BitVec a -> BitVec a
+bvUopSort :: Sort
+bvUopSort = FAbs 0 $ FFunc (bitVecSort 0) (bitVecSort 0)
+
+-- bOp :: forall a. BitVec a -> BitVec a -> BitVec a
+bvBopSort :: Sort
+bvBopSort = FAbs 0 $ FFunc (bitVecSort 0) $ FFunc (bitVecSort 0) (bitVecSort 0)
+-- bvBopSort = FAbs 0 $ FFunc (bitVecSort (FVar 0)) (FFunc (bitVecSort (FVar 0)) (bitVecSort (FVar 0)))
+
+-- cmp :: forall a. BitVec a -> BitVec a -> Bool
+bvCmpSort :: Sort
+bvCmpSort = FAbs 0 $ FFunc (bitVecSort 0) $ FFunc (bitVecSort 0) boolSort
+
+-- eq :: forall a. BitVec a -> BitVec a -> BitVec 1
+bvEqSort :: Sort
+bvEqSort = FAbs 0 $ FFunc (bitVecSort 0) $ FFunc (bitVecSort 0) (sizedBitVecSort "Size1")
+
+-- concat :: forall a b c. BitVec a -> BitVec b -> BitVec c
+bvConcatSort :: Sort
+bvConcatSort = FAbs 0 $ FAbs 1 $ FAbs 2 $
+                     FFunc (bitVecSort 0) $ FFunc (bitVecSort 1) (bitVecSort 2)
+
 interpSym :: Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
 interpSym x n t = (x, Thy x n t Theory)
 
@@ -570,8 +757,8 @@
     sx         = testSymbol x
     raw        = "is-" <> symbolRaw x
 
-symbolRaw :: Symbol -> T.Text
-symbolRaw = T.fromStrict . symbolSafeText
+symbolRaw :: Symbol -> Data.Text.Text
+symbolRaw = symbolSafeText
 
 --------------------------------------------------------------------------------
 selectSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
diff --git a/src/Language/Fixpoint/Smt/Types.hs b/src/Language/Fixpoint/Smt/Types.hs
--- a/src/Language/Fixpoint/Smt/Types.hs
+++ b/src/Language/Fixpoint/Smt/Types.hs
@@ -28,15 +28,13 @@
 
     ) where
 
-import           Control.Concurrent.Async (Async)
-import           Control.Concurrent.STM (TVar)
+import           Data.ByteString.Builder (Builder)
 import           Language.Fixpoint.Types
-import           Language.Fixpoint.Utils.Builder (Builder)
 import qualified Data.Text                as T
 import           Text.PrettyPrint.HughesPJ
+import qualified SMTLIB.Backends
 
 import           System.IO                (Handle)
-import           System.Process
 -- import           Language.Fixpoint.Misc   (traceShow)
 
 --------------------------------------------------------------------------------
@@ -93,19 +91,16 @@
                   | Error !T.Text
                   deriving (Eq, Show)
 
--- | Information about the external SMT process
+-- | Additional information around the SMT solver backend
 data Context = Ctx
-  { ctxPid     :: !ProcessHandle
-    -- | The handle for writing queries to, for input to the SMT solver.
-  , ctxIn      :: !Handle
-    -- | The handle for reading responses from, the output from the SMT solver.
-  , ctxOut     :: !Handle
+  {
+  -- | The high-level interface for interacting with the SMT solver backend.
+    ctxSolver  :: SMTLIB.Backends.Solver
+  -- | The close operation of the SMT solver backend.
+  , ctxClose   :: IO ()
   , ctxLog     :: !(Maybe Handle)
   , ctxVerbose :: !Bool
   , ctxSymEnv  :: !SymEnv
-  , ctxAsync   :: Async ()
-    -- | The next batch of queries to send to the SMT solver
-  , ctxTVar    :: TVar Builder
   }
 
 --------------------------------------------------------------------------------
diff --git a/src/Language/Fixpoint/Solver.hs b/src/Language/Fixpoint/Solver.hs
--- a/src/Language/Fixpoint/Solver.hs
+++ b/src/Language/Fixpoint/Solver.hs
@@ -98,7 +98,7 @@
 --------------------------------------------------------------------------------
 -- | Solve FInfo system of horn-clause constraints -----------------------------
 --------------------------------------------------------------------------------
-solve :: (NFData a, Fixpoint a, Show a, Loc a) => Solver a
+solve :: (PPrint a, NFData a, Fixpoint a, Show a, Loc a) => Solver a
 --------------------------------------------------------------------------------
 solve cfg q
   | parts cfg      = partition  cfg        $!! q
@@ -108,7 +108,7 @@
   | minimizeKs cfg = minKvars cfg solve'   $!! q
   | otherwise      = solve'     cfg        $!! q
 
-solve' :: (NFData a, Fixpoint a, Show a, Loc a) => Solver a
+solve' :: (PPrint a, NFData a, Fixpoint a, Show a, Loc a) => Solver a
 solve' cfg q = do
   when (save cfg) $ saveQuery   cfg q
   configSW  cfg     solveNative cfg q
@@ -181,19 +181,19 @@
 --------------------------------------------------------------------------------
 -- | Native Haskell Solver -----------------------------------------------------
 --------------------------------------------------------------------------------
-solveNative, solveNative' :: (NFData a, Fixpoint a, Show a, Loc a) => Solver a
+solveNative, solveNative' :: (NFData a, Fixpoint a, Show a, Loc a, PPrint a) => Solver a
 --------------------------------------------------------------------------------
 solveNative !cfg !fi0 = solveNative' cfg fi0
                           `catch`
                              (return . crashResult (errorMap fi0))
 
-crashResult :: ErrorMap a -> Error -> Result (Integer, a)
+crashResult :: (PPrint a) => ErrorMap a -> Error -> Result (Integer, a)
 crashResult m e = Result res mempty mempty mempty
   where
     res           = Crash es msg
     es            = catMaybes [ findError m e | e <- errs e ]
     msg | null es = showpp e
-        | otherwise = "Sorry, unexpected panic in liquid-fixpoint!"
+        | otherwise = "Sorry, unexpected panic in liquid-fixpoint!" -- ++ showpp e
 
 -- | Unpleasant hack to save meta-data that can be recovered from SrcSpan
 type ErrorMap a = HashMap.HashMap SrcSpan a
diff --git a/src/Language/Fixpoint/Solver/Instantiate.hs b/src/Language/Fixpoint/Solver/Instantiate.hs
--- a/src/Language/Fixpoint/Solver/Instantiate.hs
+++ b/src/Language/Fixpoint/Solver/Instantiate.hs
@@ -345,7 +345,7 @@
 evaluate cfg ctx aenv facts es sid = do
   let eqs      = initEqualities ctx aenv facts
   let γ        = knowledge cfg ctx aenv
-  let cands    = mytracepp  ("evaluate-cands " ++ showpp sid) $ Misc.hashNub (concatMap topApps es)
+  let cands    = mytracepp  ("evaluate-cands " ++ showpp sid) $ Misc.setNub (concatMap topApps es)
   let s0       = EvalEnv 0 [] aenv (SMT.ctxSymEnv ctx) cfg
   let ctxEqs   = [ toSMT cfg ctx [] (EEq e1 e2) | (e1, e2)  <- eqs ]
               ++ [ toSMT cfg ctx [] (expr xr)   | xr@(_, r) <- facts, null (Vis.kvarsExpr $ reftPred $ sr_reft r) ]
@@ -694,7 +694,7 @@
 initEqualities :: SMT.Context -> AxiomEnv -> [(Symbol, SortedReft)] -> [(Expr, Expr)]
 initEqualities ctx aenv es = concatMap (makeSimplifications (aenvSimpl aenv)) dcEqs
   where
-    dcEqs                  = Misc.hashNub (Mb.catMaybes [getDCEquality senv e1 e2 | EEq e1 e2 <- atoms])
+    dcEqs                  = Misc.setNub (Mb.catMaybes [getDCEquality senv e1 e2 | EEq e1 e2 <- atoms])
     atoms                  = splitPAnd . expr =<< filter isProof es
     senv                   = SMT.ctxSymEnv ctx
 
@@ -799,7 +799,7 @@
   ctx <- SMT.makeContextWithSEnv cfg file env
   _   <- SMT.smtPush ctx
   res <- k ctx
-  _   <- SMT.cleanupContext ctx
+  SMT.cleanupContext ctx
   return res
 
 infixl 9 ~>
diff --git a/src/Language/Fixpoint/Solver/Monad.hs b/src/Language/Fixpoint/Solver/Monad.hs
--- a/src/Language/Fixpoint/Solver/Monad.hs
+++ b/src/Language/Fixpoint/Solver/Monad.hs
@@ -77,7 +77,6 @@
 runSolverM cfg sI act =
   bracket acquire release $ \ctx -> do
     res <- runStateT act' (s0 ctx)
-    smtExit ctx
     return (fst res)
   where
     s0 ctx   = SS ctx be (stats0 fi)
@@ -200,15 +199,12 @@
 {-# SCC filterValid_ #-}
 filterValid_ :: F.SrcSpan -> F.Expr -> F.Cand a -> Context -> IO [a]
 filterValid_ sp p qs me = catMaybes <$> do
-  smtAssertAsync me p
-  forM_ qs $ \(q, _x) ->
-    smtBracketAsyncAt sp me "filterValidRHS" $ do
-      smtAssertAsync me (F.PNot q)
-      smtCheckUnsatAsync me
-  forM qs $ \(_, x) -> do
-    valid <- readCheckUnsat me
-    return $ if valid then Just x else Nothing
-
+  smtAssert me p
+  forM qs $ \(q, x) ->
+    smtBracketAt sp me "filterValidRHS" $ do
+      smtAssert me (F.PNot q)
+      valid <- smtCheckUnsat me
+      return $ if valid then Just x else Nothing
 
 --------------------------------------------------------------------------------
 -- | `filterValidGradual ps [(x1, q1),...,(xn, qn)]` returns the list `[ xi | p => qi]`
diff --git a/src/Language/Fixpoint/Solver/PLE.hs b/src/Language/Fixpoint/Solver/PLE.hs
--- a/src/Language/Fixpoint/Solver/PLE.hs
+++ b/src/Language/Fixpoint/Solver/PLE.hs
@@ -792,24 +792,15 @@
                 let (es1,es2) = splitAt (length (eqArgs eq)) es
                     newE = substEq env eq es1
                 (e', fe) <- evalIte γ ctx et newE -- TODO:FUEL this is where an "unfolding" happens, CHECK/BUMP counter
-                let mPLEUnfold = startsWithPLEUnfold e'
-                    e2' = Mb.fromMaybe e' mPLEUnfold
+                let e2' = stripPLEUnfold e'
                     e3' = simplify γ ctx (eApps e2' es2) -- reduces a bit the equations
                     undecidedGuards = case e' of
                       EIte{} -> True
                       _ -> False
 
-                if not undecidedGuards || Mb.isJust mPLEUnfold
+                if undecidedGuards
                   then do
-                    useFuel f
                     modify $ \st ->
-                      st
-                        { evNewEqualities = S.insert (eApps e0 es, e3') (evNewEqualities st)
-                        , evPendingUnfoldings = M.delete (eApps e0 es) (evPendingUnfoldings st)
-                        }
-                    return (Just e2', fe)
-                  else do
-                    modify $ \st ->
                       st {
                         evPendingUnfoldings = M.insert (eApps e0 es) e3' (evPendingUnfoldings st)
                       }
@@ -817,6 +808,14 @@
                     -- guarding it, just to preserve the size of further
                     -- rewrites.
                     return (Nothing, noExpand)
+                  else do
+                    useFuel f
+                    modify $ \st ->
+                      st
+                        { evNewEqualities = S.insert (eApps e0 es, e3') (evNewEqualities st)
+                        , evPendingUnfoldings = M.delete (eApps e0 es) (evPendingUnfoldings st)
+                        }
+                    return (Just e2', fe)
          else return (Nothing, noExpand)
   where
     -- At the time of writing, any function application wrapping an
@@ -824,12 +823,12 @@
     -- However, using pleUnfold still has the advantage of not generating
     -- extra equations to unfold pleUnfold itself. Using pleUnfold also
     -- makes the intention of the user rather explicit.
-    startsWithPLEUnfold e
+    stripPLEUnfold e
       | (ef, [arg]) <- splitEAppThroughECst e
       , EVar f <- dropECst ef
       , f == "Language.Haskell.Liquid.ProofCombinators.pleUnfold"
-      = Just arg
-      | otherwise = Nothing
+      = arg
+      | otherwise = e
 
 evalApp γ ctx e0 args@(e:es) _
   | EVar f <- dropECst e0
@@ -1094,7 +1093,7 @@
   ctx <- SMT.makeContextWithSEnv cfg file env
   _   <- SMT.smtPush ctx
   res <- k ctx
-  _   <- SMT.cleanupContext ctx
+  SMT.cleanupContext ctx
   return res
 
 
diff --git a/src/Language/Fixpoint/Solver/Sanitize.hs b/src/Language/Fixpoint/Solver/Sanitize.hs
--- a/src/Language/Fixpoint/Solver/Sanitize.hs
+++ b/src/Language/Fixpoint/Solver/Sanitize.hs
@@ -409,7 +409,7 @@
     env0         = F.symEnv sEnv tEnv ds lits ts
     tEnv         = Thy.theorySymbols ds
     ds           = F.ddecls si
-    ts           = Misc.hashNub (applySorts si ++ [t | (_, t) <- F.toListSEnv sEnv])
+    ts           = Misc.setNub (applySorts si ++ [t | (_, t) <- F.toListSEnv sEnv])
     sEnv         = (F.tsSort <$> tEnv) `mappend` F.fromListSEnv xts
     xts          = symbolSorts cfg si ++ alits
     lits         = F.dLits si `F.unionSEnv'` F.fromListSEnv alits
diff --git a/src/Language/Fixpoint/SortCheck.hs b/src/Language/Fixpoint/SortCheck.hs
--- a/src/Language/Fixpoint/SortCheck.hs
+++ b/src/Language/Fixpoint/SortCheck.hs
@@ -209,6 +209,7 @@
 instance (Loc a) => Elaborate (SimpC a) where
   elaborate msg env c = c {_crhs = elaborate msg' env (_crhs c) }
     where msg'        = atLoc c (val msg)
+
 --------------------------------------------------------------------------------
 -- | 'elabExpr' adds "casts" to decorate polymorphic instantiation sites.
 --------------------------------------------------------------------------------
diff --git a/src/Language/Fixpoint/Types/Config.hs b/src/Language/Fixpoint/Types/Config.hs
--- a/src/Language/Fixpoint/Types/Config.hs
+++ b/src/Language/Fixpoint/Types/Config.hs
@@ -22,6 +22,9 @@
   , Eliminate (..)
   , useElim
 
+  -- * Scrape options
+  , Scrape (..)
+
   -- * parallel solving options
   , defaultMinPartSize
   , defaultMaxPartSize
@@ -33,24 +36,24 @@
 import qualified Data.Store as S
 import qualified Data.List as L
 import Data.Serialize                (Serialize (..))
-import Control.Monad
 import Control.DeepSeq
 import GHC.Generics
 import System.Console.CmdArgs
 import System.Console.CmdArgs.Explicit
-import System.Environment
 
+import qualified Language.Fixpoint.Conditional.Z3 as Conditional.Z3
 import Language.Fixpoint.Utils.Files
 
 
 --------------------------------------------------------------------------------
 withPragmas :: Config -> [String] -> IO Config
 --------------------------------------------------------------------------------
-withPragmas = foldM withPragma
-
-withPragma :: Config -> String -> IO Config
-withPragma c s = withArgs [s] $ cmdArgsRun
-          config { modeValue = (modeValue config) { cmdArgsValue = c } }
+withPragmas c s =
+    processValueIO
+      config { modeValue = (modeValue config) { cmdArgsValue = c } }
+      s
+    >>=
+      cmdArgsApply
 
 --------------------------------------------------------------------------------
 -- | Configuration Options -----------------------------------------------------
@@ -75,6 +78,7 @@
   , allowHO     :: Bool                -- ^ allow higher order binders in the logic environment
   , allowHOqs   :: Bool                -- ^ allow higher order qualifiers
   , eliminate   :: Eliminate           -- ^ eliminate non-cut KVars
+  , scrape      :: Scrape              -- ^ configure auto-scraping of qualifiers from constraints
   , elimBound   :: Maybe Int           -- ^ maximum length of KVar chain to eliminate
   , smtTimeout  :: Maybe Int           -- ^ smt timeout in msec
   , elimStats   :: Bool                -- ^ print eliminate stats
@@ -139,20 +143,42 @@
 
 ---------------------------------------------------------------------------------------
 
-data SMTSolver = Z3 | Cvc4 | Mathsat
+data SMTSolver = Z3 | Z3mem | Cvc4 | Mathsat
                  deriving (Eq, Data, Typeable, Generic)
 
 instance Default SMTSolver where
-  def = Z3
+  def = if Conditional.Z3.builtWithZ3AsALibrary then Z3mem else Z3
 
 instance Show SMTSolver where
   show Z3      = "z3"
+  show Z3mem   = "z3 API"
   show Cvc4    = "cvc4"
   show Mathsat = "mathsat"
 
 instance S.Store SMTSolver
 
 ---------------------------------------------------------------------------------------
+-- | `Scrape` describes which (Horn) constraints to scrape qualifiers from
+--   None = do not scrape, only use the supplied qualifiers
+--   Head = scrape only from the constraint heads (i.e. "rhs")
+--   All  = scrape all concrete predicates (i.e. "rhs" + "lhs")
+
+data Scrape = No | Head | Both
+  deriving (Eq, Data, Typeable, Generic)
+
+instance Serialize Scrape
+instance S.Store Scrape
+instance NFData Scrape
+
+instance Default Scrape where
+  def = No
+
+instance Show Scrape where
+  show No   = "no"
+  show Head = "head"
+  show Both = "both"
+
+---------------------------------------------------------------------------------------
 -- | Eliminate describes the number of KVars to eliminate:
 --   None = use PA/Quals for ALL k-vars, i.e. no eliminate
 --   Some = use PA/Quals for CUT k-vars, i.e. eliminate non-cuts
@@ -199,6 +225,7 @@
   , allowHO                  = False   &= help "Allow higher order binders into fixpoint environment"
   , allowHOqs                = False   &= help "Allow higher order qualifiers"
   , eliminate                = None    &= help "Eliminate KVars [none = quals for all-kvars, cuts = quals for cut-kvars, all = eliminate all-kvars (TRUE for cuts)]"
+  , scrape                   = def     &= help "Scrape qualifiers from constraint (Horn format only) [ no = do not, head = scrape from heads, both = scrape from everywhere ]"
   , elimBound                = Nothing &= name "elimBound"   &= help "(alpha) Maximum eliminate-chain depth"
   , smtTimeout               = Nothing &= name "smtTimeout"  &= help "smt timeout in msec"
   , elimStats                = False   &= help "(alpha) Print eliminate stats"
diff --git a/src/Language/Fixpoint/Types/Constraints.hs b/src/Language/Fixpoint/Types/Constraints.hs
--- a/src/Language/Fixpoint/Types/Constraints.hs
+++ b/src/Language/Fixpoint/Types/Constraints.hs
@@ -473,8 +473,8 @@
 addIds = zipWith (\i c -> (i, shiftId i $ c {_sid = Just i})) [1..]
   where
     -- Adding shiftId to have distinct VV for SMT conversion
-    shiftId i c = c { slhs = shiftSR i $ slhs c }
-                    { srhs = shiftSR i $ srhs c }
+    shiftId i c = c { slhs = shiftSR i (slhs c) }
+                    { srhs = shiftSR i (srhs c) }
     shiftSR i sr = sr { sr_reft = shiftR i $ sr_reft sr }
     shiftR i r@(Reft (v, _)) = shiftVV r (intSymbol v i)
 
@@ -542,6 +542,7 @@
 
 instance PPrint Qualifier where
   pprintTidy k q = "qualif" <+> pprintTidy k (qName q) <+> "defined at" <+> pprintTidy k (qPos q)
+  -- pprintTidy _ q = pprQual q
 
 pprQual :: Qualifier -> Doc
 pprQual (Q n xts p l) = text "qualif" <+> text (symbolString n) <-> parens args <-> colon <+> parens (toFix p) <+> text "//" <+> toFix l
diff --git a/src/Language/Fixpoint/Types/Names.hs b/src/Language/Fixpoint/Types/Names.hs
--- a/src/Language/Fixpoint/Types/Names.hs
+++ b/src/Language/Fixpoint/Types/Names.hs
@@ -102,12 +102,12 @@
   , nilName
   , consName
   , vvName
-  , size32Name
-  , size64Name
+  , sizeName
   , bitVecName
-  , bvAndName
-  , bvOrName
+  -- , bvAndName, bvOrName, bvSubName, bvAddName
+  , intbv32Name, intbv64Name, bv32intName, bv64intName
   , propConName
+
   -- HKT , tyAppName
   , isPrim
   , prims
@@ -128,6 +128,7 @@
 
 import           Control.DeepSeq             (NFData (..))
 import           Control.Arrow               (second)
+import           Data.ByteString.Builder     (Builder)
 import           Data.Char                   (ord)
 import           Data.Maybe                  (fromMaybe)
 import           Data.Generics               (Data)
@@ -144,7 +145,7 @@
 import           Text.PrettyPrint.HughesPJ   (text)
 import           Language.Fixpoint.Types.PrettyPrint
 import           Language.Fixpoint.Types.Spans
-import           Language.Fixpoint.Utils.Builder as Builder (Builder, fromText)
+import           Language.Fixpoint.Utils.Builder as Builder (fromText)
 import Data.Functor.Contravariant (Contravariant(contramap))
 import qualified Data.Binary as B
 
@@ -546,7 +547,7 @@
 symbolBuilder = Builder.fromText . symbolSafeText . symbol
 
 {-# INLINE buildMany #-}
-buildMany :: [Builder.Builder] -> Builder.Builder
+buildMany :: [Builder] -> Builder
 buildMany []     = mempty
 buildMany [b]    = b
 buildMany (b:bs) = b <> mconcat [ " " <> b' | b' <- bs ]
@@ -618,18 +619,31 @@
 symSepName   :: (IsString a) => a
 symSepName   = "##"
 
-nilName, consName, size32Name, size64Name, bitVecName, bvOrName, bvAndName :: Symbol
-nilName      = "nil"
-consName     = "cons"
-size32Name   = "Size32"
-size64Name   = "Size64"
-bitVecName   = "BitVec"
-bvOrName     = "bvor"
-bvAndName    = "bvand"
+-- nilName, consName, size32Name, size64Name, bitVecName :: Symbol
+-- nilName      = "nil"
+-- consName     = "cons"
+-- size32Name   = "Size32"
+-- size64Name   = "Size64"
+-- bitVecName   = "BitVec"
 
--- HKT tyAppName :: Symbol
--- HKT tyAppName    = "LF-App"
+-- bvOrName, bvAndName, bvSubName, bvAddName,
+intbv32Name, intbv64Name, bv32intName, bv64intName :: Symbol
+-- bvOrName    = "bvor"
+-- bvAndName   = "bvand"
+-- bvSubName   = "bvsub"
+-- bvAddName   = "bvadd"
+intbv32Name = "int_to_bv32"
+intbv64Name = "int_to_bv64"
+bv32intName = "bv32_to_int"
+bv64intName = "bv64_to_int"
 
+nilName, consName, sizeName, bitVecName :: Symbol
+nilName       = "nil"
+consName      = "cons"
+sizeName      = "Size"
+bitVecName    = "BitVec"
+
+
 mulFuncName, divFuncName :: Symbol
 mulFuncName  = "Z3_OP_MUL"
 divFuncName  = "Z3_OP_DIV"
@@ -663,11 +677,13 @@
   , "Map_store"
   , "Map_union"
   , "Map_default"
-  , size32Name
-  , size64Name
+  -- Currently we parse X in "SizeX" to get the bitvec size
+  -- so there is no finite set of names to add here...
+  -- , size32Name
+  -- , size64Name
   , bitVecName
-  , bvOrName
-  , bvAndName
+  -- , bvOrName
+  -- , bvAndName
   , "FAppTy"
   , nilName
   , consName
diff --git a/src/Language/Fixpoint/Types/PrettyPrint.hs b/src/Language/Fixpoint/Types/PrettyPrint.hs
--- a/src/Language/Fixpoint/Types/PrettyPrint.hs
+++ b/src/Language/Fixpoint/Types/PrettyPrint.hs
@@ -93,6 +93,7 @@
 notracepp :: (PPrint a) => String -> a -> a
 notracepp _ x = x
 
+
 instance PPrint Doc where
   pprintTidy _ = id
 
@@ -111,6 +112,10 @@
 
 instance (Ord a, PPrint a, PPrint b) => PPrint (M.HashMap a b) where
   pprintTidy k = pprintKVs k . hashMapToAscList
+
+instance PPrint Char where
+  pprintTidy _ = char
+
 
 pprintKVs   :: (PPrint k, PPrint v) => Tidy -> [(k, v)] -> Doc
 pprintKVs t = vcat . punctuate "\n" . map pp1
diff --git a/src/Language/Fixpoint/Types/Refinements.hs b/src/Language/Fixpoint/Types/Refinements.hs
--- a/src/Language/Fixpoint/Types/Refinements.hs
+++ b/src/Language/Fixpoint/Types/Refinements.hs
@@ -77,7 +77,7 @@
 
   -- * Destructing
   , flattenRefas
-  , conjuncts
+  , conjuncts, concConjuncts
   , dropECst
   , eApps
   , eAppC
@@ -183,9 +183,13 @@
 reftConjuncts (Reft (v, ra)) = [Reft (v, ra') | ra' <- ras']
   where
     ras'                     = if null ps then ks else conj ps : ks  -- see [NOTE:pAnd-SLOW]
-    (ks, ps)                 = partition (\p -> isKvar p || isGradual p) $ refaConjuncts ra
+    (ps, ks)                 = partition isConc (refaConjuncts ra)
 
+isConc :: Expr -> Bool
+isConc p = not (isKvar p || isGradual p)
 
+concConjuncts :: Expr -> [Expr]
+concConjuncts e = filter isConc (refaConjuncts e)
 
 isKvar :: Expr -> Bool
 isKvar (PKVar _ _) = True
@@ -224,6 +228,8 @@
 
 refaConjuncts :: Expr -> [Expr]
 refaConjuncts p = [p' | p' <- conjuncts p, not $ isTautoPred p']
+
+
 
 --------------------------------------------------------------------------------
 -- | Kvars ---------------------------------------------------------------------
diff --git a/src/Language/Fixpoint/Types/Sorts.hs b/src/Language/Fixpoint/Types/Sorts.hs
--- a/src/Language/Fixpoint/Types/Sorts.hs
+++ b/src/Language/Fixpoint/Types/Sorts.hs
@@ -16,10 +16,7 @@
 
 -- | This module contains the data types, operations and
 --   serialization functions for representing Fixpoint's
---   implication (i.e. subtyping) and well-formedness
---   constraints in Haskell. The actual constraint
---   solving is done by the `fixpoint.native` which
---   is written in Ocaml.
+--   Horn and well-formedness constraints.
 
 module Language.Fixpoint.Types.Sorts (
 
@@ -37,10 +34,11 @@
   , setFTyCon
   , mapFTyCon -- TODO: hide these
   , mapFVar
-
   , basicSorts, intSort, realSort, boolSort, strSort, funcSort
-  , setSort, bitVecSort, mapSort, charSort
-
+  -- , bitVec32Sort, bitVec64Sort
+  , setSort, bitVecSort
+  , sizedBitVecSort
+  , mapSort, charSort
   , listFTyCon
   , isListTC
   , sizeBv
@@ -102,6 +100,7 @@
 import qualified Data.HashMap.Strict       as M
 import qualified Data.List                 as L
 import qualified Data.Binary as B
+import Text.Read (readMaybe)
 
 data FTycon   = TC LocSymbol TCInfo deriving (Ord, Show, Data, Typeable, Generic)
 
@@ -160,12 +159,10 @@
 isListTC (TC z _) = isListConName z
 
 sizeBv :: FTycon -> Maybe Int
-sizeBv tc
-  | s == size32Name = Just 32
-  | s == size64Name = Just 64
-  | otherwise       = Nothing
-  where
-    s               = val $ fTyconSymbol tc
+sizeBv tc = do
+  let s = val $ fTyconSymbol tc
+  size <- stripPrefix sizeName s
+  readMaybe $ symbolString size
 
 fTyconSymbol :: FTycon -> Located Symbol
 fTyconSymbol (TC s _) = s
@@ -485,8 +482,20 @@
 setSort :: Sort -> Sort
 setSort    = FApp (FTC setFTyCon)
 
-bitVecSort :: Sort
-bitVecSort = FApp (FTC $ symbolFTycon' bitVecName) (FTC $ symbolFTycon' size32Name)
+-- bitVecSort :: Sort -> Sort
+-- bitVecSort = FApp (FTC $ symbolFTycon' bitVecName)
+
+-- bitVec32Sort :: Sort
+-- bitVec32Sort = bitVecSort (FTC (symbolFTycon' size32Name))
+--
+-- bitVec64Sort :: Sort
+-- bitVec64Sort = bitVecSort (FTC (symbolFTycon' size64Name))
+
+bitVecSort :: Int -> Sort
+bitVecSort i = FApp (FTC $ symbolFTycon' bitVecName) (FVar i)
+
+sizedBitVecSort :: Symbol -> Sort
+sizedBitVecSort i = FApp (FTC $ symbolFTycon' bitVecName) (FTC $ symbolFTycon' i)
 
 mapSort :: Sort -> Sort -> Sort
 mapSort = FApp . FApp (FTC (symbolFTycon' mapConName))
diff --git a/src/Language/Fixpoint/Types/Theories.hs b/src/Language/Fixpoint/Types/Theories.hs
--- a/src/Language/Fixpoint/Types/Theories.hs
+++ b/src/Language/Fixpoint/Types/Theories.hs
@@ -52,21 +52,14 @@
 import qualified Data.List                as L
 import           Data.Text (Text)
 import qualified Data.Text                as Text
-import qualified Data.Text.Lazy           as LT
 import qualified Data.Store              as S
 import qualified Data.HashMap.Strict      as M
 import qualified Language.Fixpoint.Misc   as Misc
-import Data.Functor.Contravariant (Contravariant(contramap))
 
 --------------------------------------------------------------------------------
 -- | 'Raw' is the low-level representation for SMT values
 --------------------------------------------------------------------------------
-type Raw = LT.Text
-
-instance S.Store Raw where
-  peek = LT.fromStrict <$> S.peek
-  poke = S.poke . LT.toStrict
-  size = contramap LT.toStrict S.size
+type Raw = Text
 
 --------------------------------------------------------------------------------
 -- | 'SymEnv' is used to resolve the 'Sort' and 'Sem' of each 'Symbol'
diff --git a/src/Language/Fixpoint/Utils/Builder.hs b/src/Language/Fixpoint/Utils/Builder.hs
--- a/src/Language/Fixpoint/Utils/Builder.hs
+++ b/src/Language/Fixpoint/Utils/Builder.hs
@@ -3,11 +3,8 @@
 -- | Wrapper around `Data.Text.Builder` that exports some useful combinators
 
 module Language.Fixpoint.Utils.Builder
-  ( Builder
-  , fromLazyText
+  ( fromText
   , fromString
-  , fromText
-  , toLazyText
   , parens
   , (<+>)
   , parenSeqs
@@ -17,47 +14,20 @@
   , key3
   , bShow
   , bFloat
-  , bb
-  , lbb
-  , blt
   ) where
 
 import           Data.Foldable (fold)
 import           Data.String
-import qualified Data.Text.Lazy.Builder as B
-import qualified Data.Text.Lazy         as LT
+import Data.ByteString.Builder (Builder)
+import qualified Data.ByteString.Builder as B
 import qualified Data.Text              as T
+import qualified Data.Text.Encoding     as T
 import qualified Data.List              as L
 import qualified Numeric
 
--- | Offers efficient concatenation, no matter the associativity
-data Builder
-  = Node Builder Builder
-  | Leaf B.Builder
 
-instance Eq Builder where
-  b0 == b1 = toLazyText b0 == toLazyText b1
-
-instance IsString Builder where
-  fromString = Leaf . fromString
-
-instance Semigroup Builder where
-  (<>) = Node
-
-instance Monoid Builder where
-  mempty = Leaf mempty
-
-toLazyText :: Builder -> LT.Text
-toLazyText = B.toLazyText . go mempty
-  where
-    go tl (Leaf b) = b <> tl
-    go tl (Node t0 t1) = go (go tl t1) t0
-
-fromLazyText :: LT.Text -> Builder
-fromLazyText = Leaf . B.fromLazyText
-
 fromText :: T.Text -> Builder
-fromText = Leaf . B.fromText
+fromText t = B.byteString $ T.encodeUtf8 t
 
 parens :: Builder -> Builder
 parens b = "(" <>  b <> ")"
@@ -86,13 +56,3 @@
 
 bFloat :: RealFloat a => a -> Builder
 bFloat d = fromString (Numeric.showFFloat Nothing d "")
-
-bb :: LT.Text -> Builder
-bb = fromLazyText
-
-lbb :: T.Text -> Builder
-lbb = bb . LT.fromStrict
-
-blt :: Builder -> LT.Text
-blt = toLazyText
-
diff --git a/tests/pos/bitvec-ii.fq b/tests/pos/bitvec-ii.fq
new file mode 100644
--- /dev/null
+++ b/tests/pos/bitvec-ii.fq
@@ -0,0 +1,65 @@
+// This file showcases bitvector functions that in smtlib2 are
+// indexed identifiers. This means that instead of writing
+// (zero_extend 2 bv) to extend a bitvector by 2 bits, we
+// write ((_ zero_extend 2) bv).
+
+// You can see the '_' as kind of applying type level arguments.
+// In the case of 'zero_extend', it determines the size of the
+// output bitvector. 
+
+// To emulate this in liquid fixpoint, we want the output to 
+// match exactly the format of indexed identifiers of smtlib2. 
+// This comes down to defining our own '_' and parenthesizing 
+// the expression in LF exactly as we would in the smt format.
+
+// The last trick here, is that we cannot apply a parenthesized
+// expression to an expression. For this we have defined the 
+// additional expression 'app', which simply applies its operands.
+// 'app' is elaborated to the empty string to the SMT solver, such
+// that (app (_ zero_extend 2) bv) becomes ( (_ zero_extend 2) bv).
+
+bind 0 x : {v : (BitVec Size4) | v = (lit "#b1000" (BitVec Size4))}
+bind 1 y : {v : (BitVec Size4) | v = (app (_ rotate_right 7) x)}
+bind 2 z : {v : (BitVec Size4) | v = (lit "#b0001" (BitVec Size4))}
+
+constraint:
+  env [0;1;2]
+  lhs {v : (BitVec Size4) | [ v = y ] }
+  rhs {v : (BitVec Size4) | [ v = z ] }
+  id 0 tag []
+
+bind 3 y : {v : (BitVec Size6) | v = (app (_ zero_extend 2) x)}
+bind 4 z : {v : (BitVec Size6) | v = (lit "#b001000" (BitVec Size6))}
+
+constraint:
+  env [0;3;4]
+  lhs {v : (BitVec Size6) | [ v = y ] }
+  rhs {v : (BitVec Size6) | [ v = z ] }
+  id 1 tag []
+
+bind 5 y : {v : (BitVec Size6) | v = (app (_ sign_extend 2) x)}
+bind 6 z : {v : (BitVec Size6) | v = (lit "#b111000" (BitVec Size6))}
+
+constraint:
+  env [0;5;6]
+  lhs {v : (BitVec Size6) | [ v = y ] }
+  rhs {v : (BitVec Size6) | [ v = z ] }
+  id 2 tag []
+
+bind 7 y : {v : (BitVec Size8) | v = (app (_ repeat 2) x)}
+bind 8 z : {v : (BitVec Size8) | v = (lit "#b10001000" (BitVec Size8))}
+
+constraint:
+  env [0;7;8]
+  lhs {v : (BitVec Size8) | [ v = y ] }
+  rhs {v : (BitVec Size8) | [ v = z ] }
+  id 3 tag []
+
+bind 9  y : {v : (BitVec Size2) | v = (app (_ extract 3 2) x)}
+bind 10 z : {v : (BitVec Size2) | v = (lit "#b10" (BitVec Size2))}
+
+constraint:
+  env [0;9;10]
+  lhs {v : (BitVec Size2) | [ v = y ] }
+  rhs {v : (BitVec Size2) | [ v = z ] }
+  id 4 tag []
diff --git a/tests/pos/bitvec.fq b/tests/pos/bitvec.fq
new file mode 100644
--- /dev/null
+++ b/tests/pos/bitvec.fq
@@ -0,0 +1,89 @@
+bind 0 x : {v : (BitVec Size32) | [ v = (lit "#x0000000f" (BitVec Size32))]}
+bind 1 y : {v : (BitVec Size32) | [ v = (lit "#x000000f0" (BitVec Size32))]}
+bind 2 z : {v : (BitVec Size32) | [ v = (lit "#x000000ff" (BitVec Size32))]}
+
+constraint:
+  env [0;1;2]
+  lhs {v : (BitVec Size32) | [ v = bvor x y ] }
+  rhs {v : (BitVec Size32) | [ v = z ] }
+  id 0 tag []
+
+bind 4 x : {v : (BitVec Size60) | [ v = (lit "#x00000000000000f" (BitVec Size60))]}
+bind 5 y : {v : (BitVec Size60) | [ v = (lit "#x0000000000000f0" (BitVec Size60))]}
+bind 6 z : {v : (BitVec Size60) | [ v = (lit "#x000000000000000" (BitVec Size60))]}
+
+constraint:
+  env [4;5;6]
+  lhs {v : (BitVec Size60) | [ v = bvand x y ] }
+  rhs {v : (BitVec Size60) | [ v = z ] }
+  id 1 tag []
+
+bind 7 x : {v : (BitVec Size4) | [ v = (lit "#x5" (BitVec Size4))]}
+bind 8 y : {v : (BitVec Size4) | [ v = (lit "#xb" (BitVec Size4))]}
+bind 9 z : {v : (BitVec Size4) | [ v = (lit "#x1" (BitVec Size4))]}
+
+constraint:
+  env [7;8;9]
+  lhs {v : (BitVec Size4) | [ v = bvxnor x y ] }
+  rhs {v : (BitVec Size4) | [ v = z ] }
+  id 2 tag []
+
+bind 10 x : {v : (BitVec Size4) | [ v = (lit "#x4" (BitVec Size4))]}
+bind 11 y : {v : (BitVec Size4) | [ v = (lit "#xb" (BitVec Size4))]}
+
+constraint:
+  env [10;11]
+  lhs {v : (BitVec Size4) | [ v = bvnot x ] }
+  rhs {v : (BitVec Size4) | [ v = y; y != bvneg x] }
+  id 3 tag []
+
+bind 12 x : {v : (BitVec Size4) | [ v = (lit "#x4" (BitVec Size4))]}
+bind 13 y : {v : (BitVec Size4) | [ v = (lit "#xc" (BitVec Size4))]}
+
+constraint:
+  env [12;13]
+  lhs {v : (BitVec Size4) | [ v = bvneg x ] }
+  rhs {v : (BitVec Size4) | [ v = y; y != bvnot x ] }
+  id 4 tag []
+
+bind 14 x : {v : (BitVec Size4) | true }
+bind 15 y : {v : (BitVec Size4) | true }
+
+constraint:
+  env [14;15]
+  lhs {v : (BitVec Size4) | [ v = bvand x y ] }
+  rhs {v : (BitVec Size4) | [ v = bvand y x ] }
+  id 5 tag []
+
+bind 16 x : {v : (BitVec Size4) | [ v = (lit "#b1010" (BitVec Size4))]}
+bind 17 y : {v : (BitVec Size4) | [ v = (lit "#x1" (BitVec Size4))]}
+bind 18 z : {v : (BitVec Size4) | [ v = (lit "#b0101" (BitVec Size4))]}
+
+constraint:
+  env [16;17;18]
+  lhs {v : (BitVec Size4) | [ v = bvlshr x y ] }
+  rhs {v : (BitVec Size4) | [ v = z ] }
+  id 6 tag []
+
+constraint:
+  env [16;18]
+  lhs {v : (BitVec Size4) | [ v = z ] }
+  rhs {v : (BitVec Size4) | [ v = z; bvult z x ] }
+  id 7 tag []
+
+bind 19 z : {v : (BitVec Size8) | [ v = (lit "#b10100001" (BitVec Size8))]}
+
+constraint:
+  env [16;17;19]
+  lhs {v : (BitVec Size8) | [ v = concat x y ] }
+  rhs {v : (BitVec Size8) | [ v = z ] }
+  id 8 tag []
+
+constraint:
+  env [19]
+  lhs {v : (BitVec Size1) | [ v = bvcomp z z ] }
+  rhs {v : (BitVec Size1) | [ v = (lit "#b1" (BitVec Size1)) ] }
+  id 9 tag []
+
+
+
diff --git a/tests/pos/meas00.fq b/tests/pos/meas00.fq
--- a/tests/pos/meas00.fq
+++ b/tests/pos/meas00.fq
@@ -1,5 +1,4 @@
-qualif Sz(v: Tree): (0 < thinginess v)
-qualif Sz(v: Tree): (1 < 0)
+fixpoint "--eliminate=some"
 
 constant thinginess : func(0, [Tree; int])
 
@@ -16,6 +15,6 @@
   rhs {v : Tree | 0 < thinginess v }
   id 2 tag []
 
-wf: 
+wf:
   env [ ]
   reft { v: Tree | $k1 }
diff --git a/tests/test.hs b/tests/test.hs
--- a/tests/test.hs
+++ b/tests/test.hs
@@ -7,6 +7,7 @@
 import qualified Control.Concurrent.STM as STM
 import qualified Data.Functor.Compose   as Functor
 import qualified Data.IntMap            as IntMap
+import Control.Monad (when)
 import qualified Control.Monad.State    as State
 import Control.Monad.Trans.Class (lift)
 
@@ -134,11 +135,14 @@
         assertEqual "" True True
       else do
         createDirectoryIfMissing True $ takeDirectory log
-        withFile log WriteMode $ \h -> do
+        c <- withFile log WriteMode $ \h -> do
           let cmd     = testCmd opts "fixpoint" dir file
           (_,_,_,ph) <- createProcess $ (shell cmd) {std_out = UseHandle h, std_err = UseHandle h}
-          c          <- waitForProcess ph
-          assertEqual "Wrong exit code" code c
+          waitForProcess ph
+        when (code /= c) $
+          readFile log >>= putStrLn
+        assertEqual "Wrong exit code" code c
+
   where
     test = dir </> file
     log  = let (d,f) = splitFileName file in dir </> d </> ".liquid" </> f <.> "log"