diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -2,6 +2,25 @@
 
 ## NEXT
 
+## 0.9.6.3.6 (2026-05-06)
+
+- Drop dependency on lens-family [#841](http://github.com/ucsd-progsys/liquid-fixpoint/pull/841)
+- Add sort-compatibility check for measure application in PLE [#840](https://github.com/ucsd-progsys/liquid-fixpoint/pull/840)
+- Eagerly expand the body of eta-expanded terms [#838](https://github.com/ucsd-progsys/liquid-fixpoint/pull/838)
+- Add polymorphic kvar type variable substitution [#837](https://github.com/ucsd-progsys/liquid-fixpoint/pull/837)
+- Show wf constraints in prettified fixpoint queries [#836](https://github.com/ucsd-progsys/liquid-fixpoint/pull/836)
+- Unapply solutions in fqout files for readability [#835](https://github.com/ucsd-progsys/liquid-fixpoint/pull/835)
+- Wildcard literals in qualifiers in horn constraints. [#834](https://github.com/ucsd-progsys/liquid-fixpoint/pull/834)
+- Produce a fqout file before PLE [#835](https://github.com/ucsd-progsys/liquid-fixpoint/pull/835)
+- Add `--save-dir` flag to specify output directory for generated files [#832](https://github.com/ucsd-progsys/liquid-fixpoint/pull/832)
+- Add `--save-bfq-on-error` flag to collect .bfq files on verification failure [#831](https://github.com/ucsd-progsys/liquid-fixpoint/pull/831)
+- Escape SMT string literals [#828](https://github.com/ucsd-progsys/liquid-fixpoint/pull/828)
+- Add `cut` support to Horn query parser [#827](https://github.com/ucsd-progsys/liquid-fixpoint/pull/827)
+- Fix name captures in substitution of PExist and PAll [#826](https://github.com/ucsd-progsys/liquid-fixpoint/pull/826)
+- Don't require a space after the comment start [#825](https://github.com/ucsd-progsys/liquid-fixpoint/pull/825)
+- Add support for fractional literals [#822](https://github.com/ucsd-progsys/liquid-fixpoint/pull/822) [#824](https://github.com/ucsd-progsys/liquid-fixpoint/pull/824)
+- Generalize expressions and substitutions over binding types [#763](https://github.com/ucsd-progsys/liquid-fixpoint/pull/763)
+
 ## 0.9.6.3.5 (2026-01-14)
 
 - Implement `--sortedsolution` to keep elaborated sorts in fqout/solution [#821](https:://github.com/ucsd-progsys/liquid-fixpoint/pull/821)
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -250,19 +250,18 @@
   The important bit is that a `KVar` i.e. terms of the form
 
 ```
-     $k1[x1:=y1][x2:=y2]...[xn:=yn]
+    $k1[@a:=b;a2:=b2][x1:=y1][x2:=y2]...[xn:=yn]
 ```
 
-  That is represented in the `Expr` type as
+  that is represented in the `Expr` type as
 
 ```
-  | PKVar  !KVar !Subst
+  | PKVar  KVar TyVarSubst Subst
 ```
 
   must appear _only_ at the **top-level** that is not under _any_
   other operators, i.e. not as a sub-`Expr` of other expressions.
 
-
 - This is basically a predicate that needs to be "well sorted"
   with respect to the `BindId`, intuitively
 
@@ -306,6 +305,14 @@
 
 ```
     $k_##42 [x:=e1][y:=e2][v:=e3]
+```
+
+Additionally the `KVar` could have a substitution of type variables if it appears
+in the return type of a type application (e.g. `f @b` with
+`f : forall a. {v1:[a] | $k_##42[v:=v1]}`).
+
+```
+  f @b : {v1:[b] | $k_##42[@a:=b][v:=v1] }
 ```
 
 ### Global vs. Distinct Literals
diff --git a/bin/Fixpoint.hs b/bin/Fixpoint.hs
--- a/bin/Fixpoint.hs
+++ b/bin/Fixpoint.hs
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.6.3.5
+version:            0.9.6.3.6
 synopsis:           Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
 description:
   This package implements an SMTLIB based Horn-Clause\/Logical Implication constraint
@@ -25,7 +25,7 @@
 license:            BSD-3-Clause
 license-file:       LICENSE
 build-type:         Simple
-tested-with:        GHC == 9.12.2, GHC == 9.10.1, GHC == 9.8.2
+tested-with:        GHC == 9.14.1, GHC == 9.12.2, GHC == 9.10.1, GHC == 9.8.2
 extra-source-files: tests/neg/*.fq
                     tests/pos/*.fq
                     unix/Language/Fixpoint/Utils/*.hs
@@ -98,6 +98,7 @@
                     Language.Fixpoint.Solver.Worklist
                     Language.Fixpoint.SortCheck
                     Language.Fixpoint.Types
+                    Language.Fixpoint.Types.Binders
                     Language.Fixpoint.Types.Config
                     Language.Fixpoint.Types.Constraints
                     Language.Fixpoint.Types.Environments
@@ -144,7 +145,6 @@
                   , gitrev              >= 1.3.1
                   , hashable
                   , intern
-                  , lens-family
                   , megaparsec           >= 7.0.0 && < 10
                   , mtl
                   , parser-combinators
diff --git a/src/Language/Fixpoint/Graph/Deps.hs b/src/Language/Fixpoint/Graph/Deps.hs
--- a/src/Language/Fixpoint/Graph/Deps.hs
+++ b/src/Language/Fixpoint/Graph/Deps.hs
@@ -352,11 +352,12 @@
 --------------------------------------------------------------------------------
 type EdgeRank = M.HashMap F.KVar Integer
 --------------------------------------------------------------------------------
+-- | Builds a map from KVar to the _smallest_ ConstraintID that KVar appears in LHS of
 edgeRank :: [CEdge] -> EdgeRank
 edgeRank es = minimum . (n :) <$> kiM
   where
-    n       = 1 + maximum [ i | (Cstr i, _)     <- es ]
-    kiM     = group [ (k, i) | (KVar k, Cstr i) <- es ]
+    n       = 1 + maximum [ i | (Cstr i, _)     <- es ] -- number larger than maximum constraint id
+    kiM     = group [ (k, i) | (KVar k, Cstr i) <- es ] -- map each `k` to cstrs in which it appears on LHS
 
 edgeRankCut :: EdgeRank -> Cutter CVertex
 edgeRankCut km vs = case ks of
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
@@ -7,6 +7,7 @@
 
 import           Data.Ord (Down(..), comparing)
 import qualified Data.HashMap.Strict            as M
+import qualified Data.HashSet                   as S
 import qualified Data.List                      as L
 import qualified Data.Tuple                     as Tuple
 import           GHC.Generics                   (Generic)
@@ -28,6 +29,7 @@
   , F.ddecls    = H.qData q
   , F.hoInfo    = F.cfgHoInfo cfg
   , F.defns     = F.MkDefinedFuns (H.qDefs q)
+  , F.kuts      = F.KS (S.fromList (H.qKuts q))
   }
   where
     be0         = F.emptyBindEnv
@@ -104,9 +106,9 @@
     go (H.PAnd  ps) = F.PAnd (go <$> ps)
 
 kvApp :: KVEnv a -> F.Symbol -> [F.Expr] -> F.Expr
-kvApp kve k ys = F.PKVar (F.KV k) su
+kvApp kve k ys = F.PKVar (F.KV k) M.empty su
   where
-    su         = F.mkSubst (zip params ys)
+    su         = F.mkKVarSubst (zip params ys)
     params     = maybe err1 kvParams (M.lookup k kve)
     err1       = F.panic ("Unknown Horn variable: " ++ F.showpp k)
 
@@ -123,7 +125,7 @@
 kvInfo be k       = (be', KVInfo k (Misc.fst3 <$> xts) wfc)
   where
     -- make the WfC
-    wfc           = F.WfC wenv wrft  (H.hvMeta k)
+    wfc           = F.WfC wenv wrft (H.hvMeta k)
     wenv          = F.fromListIBindEnv ids
     wrft          = (x, t, F.KV (H.hvName k))
     -- add the binders
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
@@ -11,7 +11,7 @@
   , sortP
 ) where
 
-import qualified Language.Fixpoint.Parse        as FP (Parser, addNumTyCon, lexeme', locLexeme', reserved', reservedOp', symbolR, upperIdR, lowerIdR, stringR, naturalR, mkFTycon)
+import qualified Language.Fixpoint.Parse        as FP (Parser, addNumTyCon, lexeme', locLexeme', reserved', reservedOp', symbolR, upperIdR, lowerIdR, stringR, naturalR, mkFTycon, kvarP)
 import qualified Language.Fixpoint.Types        as F
 import qualified Language.Fixpoint.Horn.Types   as H
 import           Text.Megaparsec                hiding (State)
@@ -137,6 +137,7 @@
   , H.qData  =              [ dd    | HDat dd  <- things ]
   , H.qOpts  =              [ o     | HOpt o   <- things ]
   , H.qNums  =              [ s     | HNum s   <- things ]
+  , H.qKuts  =              [ k     | HKut k   <- things ]
   }
 
 -- | A @HThing@ describes the kinds of things we may see, in no particular order
@@ -156,6 +157,7 @@
   | HDat !F.DataDecl
   | HOpt !String
   | HNum  F.Symbol
+  | HKut  F.KVar
   deriving (Functor)
 
 hThingP :: FParser (HThing H.Tag)
@@ -172,6 +174,7 @@
         <|> HMat  <$> (reserved "match"      *> matchP)
         <|> HDat  <$> (reserved "datatype"   *> dataDeclP)
         <|> HNum  <$> (reserved "numeric"    *> numericDeclP)
+        <|> HKut  <$> (reserved "cut"        *> FP.kvarP)
 
 numericDeclP :: FParser F.Symbol
 numericDeclP = do
@@ -218,7 +221,9 @@
   return  $ F.mkQual n (mkParam <$> params) body pos
 
 mkParam :: (F.Symbol, F.Sort) -> F.QualParam
-mkParam (x, t) = F.QP x F.PatNone t
+mkParam (x, t) = case F.stripSuffix (F.symbol (T.pack "#")) x of
+  Just x' -> F.QP x' F.PatLit  t
+  Nothing -> F.QP x  F.PatNone t
 
 -------------------------------------------------------------------------------
 -- | Horn Variables
diff --git a/src/Language/Fixpoint/Horn/Transformations.hs b/src/Language/Fixpoint/Horn/Transformations.hs
--- a/src/Language/Fixpoint/Horn/Transformations.hs
+++ b/src/Language/Fixpoint/Horn/Transformations.hs
@@ -476,7 +476,7 @@
 
 predToExpr :: Pred -> F.Expr
 predToExpr (Reft e) = e
-predToExpr (Var k xs) = F.PKVar (F.KV k) (F.Su $ M.fromList su)
+predToExpr (Var k xs) = F.PKVar (F.KV k) M.empty (F.toKVarSubst $ M.fromList su)
   where su = zip (kargs k) xs
 predToExpr (PAnd ps) = F.PAnd $ predToExpr <$> ps
 
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
@@ -217,6 +217,7 @@
   , qData  :: ![F.DataDecl]              -- ^ list of data-declarations
   , qOpts  :: ![String]                  -- ^ list of fixpoint options
   , qNums  :: ![F.Symbol]                -- ^ list of numeric TyCon (?)
+  , qKuts  :: ![F.KVar]                  -- ^ list of cut variables
   }
   deriving (Data, Typeable, Generic, Functor, ToJSON, FromJSON)
 
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
@@ -85,9 +85,9 @@
 -- | Edit Distance --------------------------------------------
 ---------------------------------------------------------------
 
-{-# SCC editDistance #-}
-editDistance :: Eq a => [a] -> [a] -> Int
-editDistance xs ys = table ! (m, n)
+{-# SCC levenshteinDistance #-}
+levenshteinDistance :: Eq a => [a] -> [a] -> Int
+levenshteinDistance xs ys = table ! (m, n)
     where
     (m,n) = (length xs, length ys)
     x     = array (1,m) (zip [1..] xs)
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
@@ -49,6 +49,7 @@
   , mkQual      -- constructing qualifiers
   , infixSymbolP -- parse infix symbols
   , locInfixSymbolP
+  , kvarP
 
   -- * Parsing recursive entities
   , exprP        -- Expressions
@@ -555,12 +556,12 @@
 -- | Consumes a line comment.
 lhLineComment :: ParserV v ()
 lhLineComment =
-  L.skipLineComment "// "
+  L.skipLineComment "//"
 
 -- | Consumes a block comment.
 lhBlockComment :: ParserV v ()
 lhBlockComment =
-  L.skipBlockComment "/* " "*/"
+  L.skipBlockCommentNested "/*" "*/"
 
 -- | Parser that consumes a single char within an identifier (not start of identifier).
 identLetter :: ParserV v Char
@@ -776,12 +777,12 @@
 -- parse names as LocSymbol as well, this class can be eliminated.
 class (Fixpoint v, Ord v) => ParseableV v where
   parseV :: ParserV v v
-  mkSu :: [(Symbol, ExprV v)] -> SubstV v
+  mkSu :: [(Symbol, ExprV v)] -> KVarSubst Symbol v
   vFromString :: Located String -> v
 
 instance ParseableV Symbol where
   parseV = symbolP
-  mkSu = mkSubst
+  mkSu = mkKVarSubst
   vFromString = symbol
 
 -- | Parser for "atomic" expressions.
@@ -1073,6 +1074,7 @@
   <|> (reserved "real"    >> return realFTyCon)
   <|> (reserved "bool"    >> return boolFTyCon)
   <|> (reserved "num"     >> return numFTyCon)
+  <|> (reserved "frac"    >> return fracFTyCon)
   <|> (reserved "Str"     >> return strFTyCon)
   <|> (mkFTycon          =<<  locUpperIdP)
 
@@ -1095,16 +1097,32 @@
 falseP = reserved "false" >> return PFalse
 
 kvarPredP :: ParseableV v => ParserV v (ExprV v)
-kvarPredP = PKVar <$> kvarP <*> substP
+kvarPredP = do
+  k   <- kvarP
+  tsu <- tySubP
+  PKVar k tsu <$> substP
 
 kvarP :: ParserV v KVar
 kvarP = KV <$> lexeme (char '$' *> symbolR)
 
-substP :: ParseableV v => ParserV v (SubstV v)
+substP :: ParseableV v => ParserV v (KVarSubst Symbol v)
 substP = mkSu <$> many (brackets $ pairP symbolP aP exprP)
   where
     aP = reservedOp ":="
 
+-- | Parses the type-variable substitution section of a PKVar expression.
+-- An empty section looks like @[@]@; a non-empty one like @[\@sym:=sort;...]@.
+-- Returns an empty map if neither form is found (backward compat).
+tySubP :: ParserV v (M.HashMap Symbol Sort)
+tySubP = try tySub <|> pure M.empty
+  where
+    tySub = brackets (char '@' >> (M.fromList <$> sepBy1 tyPairP (sym ";")))
+    tyPairP = do
+      s <- symbolP
+      _ <- reservedOp ":="
+      t <- sortP
+      return (s, t)
+
 -- | Parses a semicolon-separated bracketed list of predicates.
 --
 -- Used as the argument of the prefix-versions of conjunction and
@@ -1558,4 +1576,3 @@
 
 instance Inputable [Command] where
   rr' = doParse' commandsP
-
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
@@ -65,7 +65,7 @@
     ) where
 
 import           Language.Fixpoint.Types.Config ( SMTSolver (..), solverFlags
-                                                , Config (solver, smtTimeout, noStringTheory, save, allowHO))
+                                                , Config (solver, smtTimeout, noStringTheory, save, saveDir, allowHO))
 import qualified Language.Fixpoint.Misc          as Misc
 import           Language.Fixpoint.Types.Errors
 import           Language.Fixpoint.Utils.Files
@@ -278,7 +278,7 @@
                LBS.hPutStr hLog "\n"
        return me
     where
-       smtFile = extFileName Smt2 f
+       smtFile = extFileNameR' (saveDir cfg) Smt2 f
 
 makeContextWithSEnv :: Config -> FilePath -> SymEnv -> DefinedFuns -> IO Context
 makeContextWithSEnv cfg f env defns = do
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
@@ -25,6 +25,8 @@
 -- import           Data.Text.Format
 import           Language.Fixpoint.Misc (sortNub, errorstar)
 import           Language.Fixpoint.Utils.Builder as Builder
+import qualified Data.Text as T
+import Data.Text (Text)
 -- import Debug.Trace (trace)
 
 instance SMTLIB2 (Symbol, Sort) where
@@ -125,7 +127,19 @@
   smt2 = smt2 . val
 
 instance SMTLIB2 SymConst where
-  smt2 = smt2 . symbol
+  smt2 c@(SL t) = do
+    seStr <- gets seString
+    if seStr
+      then pure $ quotes $ fromText $ smtEscape t  -- emit "hello" not lit$36$hello
+      else smt2 (symbol c)
+
+-- | Per https://smt-lib.org/theories-UnicodeStrings.shtml
+-- "SMT-LIB 2.6 has one escape sequence of its own for string literals. Two
+--  double quotes ("") are used to represent the double-quote character within
+--  a string literal"
+
+smtEscape :: Text -> Text
+smtEscape = T.replace "\"" "\"\""
 
 instance SMTLIB2 Constant where
   smt2 (I n)   = pure $ bShow n
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
@@ -59,6 +59,7 @@
 import qualified Language.Fixpoint.Types as Types (GInfo(..))
 import           Language.Fixpoint.Minimize (minQuery, minQuals, minKvars)
 import           Control.DeepSeq
+import           Data.Functor                        (void)
 import qualified Data.ByteString as B
 import Data.Maybe (catMaybes)
 import qualified Text.PrettyPrint.HughesPJ as PJ
@@ -116,11 +117,13 @@
   :: (PPrint a, NFData a, Fixpoint a, Show a, Loc a)
   => Config -> FInfo a -> IO (Result (Integer, a))
 solve' cfg q = do
-  when (save cfg) $ saveQuery   cfg q
-  if multicore cfg then
-    solvePar cfg q
-  else
-    solveNative cfg (slice cfg q)
+    when (save cfg) $ saveQuery cfg q
+    res <- if multicore cfg then
+             solvePar cfg q
+           else
+             solveNative cfg (slice cfg q)
+    when (saveBfqOnError cfg && isUnsafe res) $ saveBinaryQuery cfg (void q)
+    return res
 
 --------------------------------------------------------------------------------
 readFInfo :: FilePath -> IO (FInfo (), [String])
@@ -287,7 +290,7 @@
   -- rnf soln `seq` donePhase Loud "Solve2"
   --let stat = resStatus res
   -- saveSolution cfg res
-  when (save cfg) $ saveSolution cfg res
+  when (save cfg) $ Sol.saveSolution cfg "" res
   -- writeLoud $ "\nSolution:\n"  ++ showpp (resSolution res)
   -- colorStrLn (colorResult stat) (show stat)
   return res
@@ -306,28 +309,6 @@
   return $ mempty { Types.quals = Types.quals  fi
                   , Types.gLits = Types.gLits  fi
                   , Types.dLits = Types.dLits  fi }
-
-saveSolution :: Config -> Result a -> IO ()
-saveSolution cfg res = when (save cfg) $ do
-  let f = queryFile Out cfg
-  putStrLn $ "Saving Solution: " ++ f ++ "\n"
-  ensurePath f
-  writeFile f $ unlines $
-    [ ""
-    , "Solution:"
-    , scopedRender (resSolution  res)
-    ] ++
-    [ ""
-    , ""
-    , "Non-cut kvars:"
-    , ""
-    , scopedRender (HashMap.map forceDelayed $ resNonCutsSolution res)
-    ]
-    where
-      scopedRender = PJ.render . PJ.vcat . map ncDoc . scoped
-      scoped sol = [ (k, scope k, e) | (k, e) <- HashMap.toList sol]
-      scope k = HashMap.lookupDefault [] k $ resSorts res
-      ncDoc (k, xts, e) = PJ.hsep [ pprint k PJ.<> pprint xts, ":=", pprint e ]
 
 simplifyResult :: Config -> Result a -> Result a
 simplifyResult cfg res =
diff --git a/src/Language/Fixpoint/Solver/Eliminate.hs b/src/Language/Fixpoint/Solver/Eliminate.hs
--- a/src/Language/Fixpoint/Solver/Eliminate.hs
+++ b/src/Language/Fixpoint/Solver/Eliminate.hs
@@ -111,12 +111,12 @@
     cs            = getSubC   si <$> M.lookupDefault [] k kI
 
 nonCutCube :: SimpC a -> Sol.Cube
-nonCutCube c = Sol.Cube (senv c) (rhsSubst c) (subcId c) (stag c)
+nonCutCube c = Sol.Cube (senv c) (substFromKSubst $ rhsSubst c) (subcId c) (stag c)
 
-rhsSubst :: SimpC a -> Subst
+rhsSubst :: SimpC a -> KVarSubst Symbol Symbol
 rhsSubst             = rsu . crhs
   where
-    rsu (PKVar _ su) = su
+    rsu (PKVar _ _ su) = su
     rsu _            = errorstar "Eliminate.rhsSubst called on bad input"
 
 getSubC :: SInfo a -> Integer -> SimpC a
diff --git a/src/Language/Fixpoint/Solver/EnvironmentReduction.hs b/src/Language/Fixpoint/Solver/EnvironmentReduction.hs
--- a/src/Language/Fixpoint/Solver/EnvironmentReduction.hs
+++ b/src/Language/Fixpoint/Solver/EnvironmentReduction.hs
@@ -37,6 +37,8 @@
 #else
 import           Data.List (foldl', partition)
 #endif
+import           Data.Functor.Const (Const(..))
+import           Data.Functor.Identity (Identity(..))
 import           Data.Maybe (fromMaybe)
 import           Data.ShareMap (ShareMap)
 import qualified Data.ShareMap as ShareMap
@@ -72,12 +74,11 @@
 import           Language.Fixpoint.Types.PrettyPrint
 import           Language.Fixpoint.Types.Refinements
   ( Brel(..)
-  , ExprV(..)
+  , ExprBV(..)
   , Expr
   , KVar(..)
   , SortedReft(..)
-  , Subst
-  , SubstV(..)
+  , KVarSubst
   , pattern PTrue
   , pattern PFalse
   , dropECst
@@ -91,11 +92,10 @@
   , reftPred
   , sortedReftSymbols
   , subst1
+  , fromKVarSubst
   )
 import           Language.Fixpoint.Types.Sorts (boolSort, sortSymbols)
 import           Language.Fixpoint.Types.Visitor (mapExprOnExpr)
-import           Lens.Family2 (Lens', view, (%~))
-import           Lens.Family2.Stock (_2)
 import Language.Fixpoint.Misc (snd3)
 
 -- | Strips from all the constraint environments the bindings that are
@@ -399,7 +399,7 @@
    in
       (bindIdsByKVar, substsByKVar, kvarsBySubC)
   where
-    kvarsByBindId :: HashMap BindId (HashMap KVar [Subst])
+    kvarsByBindId :: HashMap BindId (HashMap KVar [KVarSubst Symbol Symbol])
     kvarsByBindId =
       HashMap.map (exprKVars . reftPred . sr_reft . snd3) $ beBinds bindEnv
 
@@ -408,9 +408,8 @@
     kvarBindsFromSubC :: ReducedConstraint a -> HashMap KVar (HashSet Symbol)
     kvarBindsFromSubC sc =
       let c = originalConstraint sc
-          unSubst (Su su) = su
           substsToHashSet =
-            HashSet.fromMap . HashMap.map (const ()) . HashMap.unions . map unSubst
+            HashSet.fromMap . HashMap.map (const ()) . HashMap.unions . map fromKVarSubst
        in foldl' (HashMap.unionWith HashSet.union) HashMap.empty $
           map (HashMap.map substsToHashSet) $
           (exprKVars (reftPred $ sr_reft $ srhs c) :) $
@@ -572,6 +571,23 @@
           ]
         )
 
+-- lens
+--
+-- We use internally the following lens to modify the SortedReft in the
+-- environment. This was imported from lens-family, but we don't want to depend
+-- on the whole library for just these few definitions.
+
+type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s
+
+_2 :: Lens' (a, b) b
+_2 f (a, b) = fmap (a,) (f b)
+
+view :: Lens' s a -> s -> a
+view l s = getConst (l Const s)
+
+(%~) :: Lens' s a -> (a -> a) -> s -> s
+(%~) l f s = runIdentity (l (Identity . f) s)
+
 -- | Inlines some of the bindings whose symbol satisfies a given predicate.
 --
 -- Only works if the bindings don't form cycles.
@@ -584,7 +600,7 @@
 substBindingsSimplifyingWith simplifier vLens p env =
     -- Circular program here. This should terminate as long as the
     -- bindings introduced by ANF don't form cycles.
-    let env' = HashMap.map (vLens %~ simplifier . inlineInSortedReft (srLookup filteredEnv)) env
+    let env' = HashMap.map (vLens %~ (simplifier . inlineInSortedReft (srLookup filteredEnv))) env
         filteredEnv = HashMap.filterWithKey (\sym _v -> p sym) env'
      in env'
   where
diff --git a/src/Language/Fixpoint/Solver/Extensionality.hs b/src/Language/Fixpoint/Solver/Extensionality.hs
--- a/src/Language/Fixpoint/Solver/Extensionality.hs
+++ b/src/Language/Fixpoint/Solver/Extensionality.hs
@@ -137,7 +137,7 @@
     go p e@(ESym _)      = f p e
     go p e@(ECon _)      = f p e
     go p e@(EVar _)      = f p e
-    go p e@(PKVar _ _)   = f p e
+    go p e@(PKVar {})      = f p e
     go p (ENeg e)        = f p . ENeg =<< go p e
     go p (ECst e t)      = f p . (`ECst` t) =<< go p e
     go p (ECoerc a t e)  = f p . ECoerc a t =<< go p e
@@ -169,7 +169,7 @@
     go e@(ESym _)        = e
     go e@(ECon _)        = e
     go e@(EVar _)        = e
-    go e@(PKVar _ _)     = e
+    go e@(PKVar {})        = e
     go e@(ENeg _)        = e
     go (PNot e)          = PImp e PFalse
     go e@(ECst _ _)      = e
diff --git a/src/Language/Fixpoint/Solver/Interpreter.hs b/src/Language/Fixpoint/Solver/Interpreter.hs
--- a/src/Language/Fixpoint/Solver/Interpreter.hs
+++ b/src/Language/Fixpoint/Solver/Interpreter.hs
@@ -136,7 +136,8 @@
   where
     withRewrites exprs =
       let
-        rws = [rewrite e rw | rw <- snd <$> M.toList (knSims γ)
+        sortEnv = seSort (evEnv env)
+        rws = [rewrite sortEnv e rw | rw <- snd <$> M.toList (knSims γ)
                             ,  e <- S.toList (snd `S.map` exprs)]
       in
         exprs <> S.fromList (concat rws)
@@ -162,8 +163,8 @@
   res <- evalOne env γ env' ictx e
   return (ictx, res : acc)
 
-rewrite :: Expr -> Rewrite -> [(Expr,Expr)]
-rewrite e rw = Mb.mapMaybe (`rewriteTop` rw) (notGuardedApps e)
+rewrite :: SEnv Sort -> Expr -> Rewrite -> [(Expr,Expr)]
+rewrite env e rw = filter (wellSorted env . fst) $ Mb.mapMaybe (`rewriteTop` rw) (notGuardedApps e)
 
 rewriteTop :: Expr -> Rewrite -> Maybe (Expr,Expr)
 rewriteTop e rw
@@ -174,6 +175,10 @@
   | otherwise
   = Nothing
 
+-- | Check that an expression is well-sorted
+wellSorted :: SEnv Sort -> Expr -> Bool
+wellSorted env = Mb.isJust . checkSortExpr dummySpan env
+
 ----------------------------------------------------------------------------------------------
 -- | Step 3: @resSInfo@ uses incremental PLE result @InstRes@ to produce the strengthened SInfo
 ----------------------------------------------------------------------------------------------
@@ -262,8 +267,9 @@
           , icSubcId = cidMb -- fst <$> L.find (\(_, b) -> (head delta) `memberIBindEnv` (_cenv b)) ieCstrs
           }                  -- eliminate above if nothing broken
   where
-    initEqs   = S.fromList $ concat [rewrite e rw | e  <- cands ++ (snd <$> S.toList (icEquals ctx))
+    initEqs   = S.fromList $ concat [rewrite sortEnv e rw | e  <- cands ++ (snd <$> S.toList (icEquals ctx))
                                                   , rw <- snd <$> M.toList (knSims ieKnowl)]
+    sortEnv   = seSort (evEnv ieEvEnv)
     cands     = concatMap (makeCandidates ieKnowl ctx) (rhs:es)
     sims      = S.filter (isSimplification (knDCs ieKnowl)) (initEqs <> icEquals ctx)
     econsts   = M.fromList $ findConstants ieKnowl es
@@ -365,7 +371,7 @@
       ELam _ _ -> acc
       ETApp _ _ -> acc
       ETAbs _ _ -> acc
-      PKVar _ _ -> acc
+      PKVar {} -> acc
       PAll _ _ -> acc
       PExist _ _ -> acc
 
@@ -392,7 +398,7 @@
       ELam _ _ -> acc
       ETApp _ _ -> acc
       ETAbs _ _ -> acc
-      PKVar _ _ -> acc
+      PKVar {} -> acc
       PAll _ _ -> acc
       PExist _ _ -> acc
 
@@ -547,7 +553,7 @@
 interpret ie γ ctx env (PAtom o e1 e2)  = let e1' = interpret' ie γ ctx env e1
                                               e2' = interpret' ie γ ctx env e2 in
                                             applyBooleanFolding o e1' e2'
-interpret _  _ _   _   e@(PKVar _ _)    = e
+interpret _  _ _   _   e@(PKVar {})       = e
 interpret ie γ ctx env e@(PAll xss e1)  = case xss of
   [] -> interpret' ie γ ctx env e1
   _  -> e
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
@@ -705,6 +705,8 @@
 
 data EvalType =
     NoRW       -- Normal PLE
+  | NoRWEta    -- Like Normal PLE but we keep track that we are in an eta
+               -- expansion context
   | FuncNormal -- REST: Expand function definitions only when the branch can be decided
   | RWNormal   -- REST: Fully Expand Defs in the context of rewriting (similar to NoRW)
   deriving (Eq)
@@ -788,24 +790,30 @@
     isEtaSymbol = isPrefixOfSym "eta"
 
 evalELam γ ctx et (x, s) e = do
-    oldPendingUnfoldings <- gets evPendingUnfoldings
-    oldEqs <- gets evNewEqualities
+  e' <- evalInExtendedEnv [(x, s)] γ ctx et e
+  let elam = ELam (x, s) e
+  modify $ \st -> st
+    { evNewEqualities = S.insert (elam, ELam (x, s) e') (evNewEqualities st) }
+  return (ELam (x, s) e')
 
-    -- We need to declare the variable in the environment
-    modify $ \st -> st
-      { evEnv = insertSymEnv x s $ evEnv st }
+evalInExtendedEnv :: [(Symbol, Sort)] -> Knowledge -> ICtx -> EvalType -> Expr -> EvalST Expr
+evalInExtendedEnv binds γ ctx et e = do
+  oldPendingUnfoldings <- gets evPendingUnfoldings
+  oldEqs               <- gets evNewEqualities
+  -- We need to declare the variables in the environment
+  modify $ \st -> st
+    { evEnv = insertsSymEnv (evEnv st) binds }
+  e' <- eval (γ { knLams = binds ++ knLams γ }) ctx et e
+  let e'' = simplify γ ctx e'
+  -- Discard the old equalities which miss the lambda binding
+  modify $ \st -> st
+    { evPendingUnfoldings = oldPendingUnfoldings
+    , evNewEqualities = oldEqs
+    -- Leaving the scope thus we need to get rid of it
+    , evEnv = deletesSymEnv (evEnv st) (map fst binds)
+    }
+  pure e''
 
-    e' <- eval (γ { knLams = (x, s) : knLams γ }) ctx et e
-    let e2' = simplify γ ctx e'
-        elam = ELam (x, s) e
-    -- Discard the old equalities which miss the lambda binding
-    modify $ \st -> st
-      { evPendingUnfoldings = oldPendingUnfoldings
-      , evNewEqualities = S.insert (elam, ELam (x, s) e2') oldEqs
-      -- Leaving the scope thus we need to get rid of it
-      , evEnv = deleteSymEnv x $ evEnv st
-      }
-    return (ELam (x, s) e')
 
 data RESTParams oc = RP
   { oc   :: OCAlgebra oc Expr IO
@@ -1076,11 +1084,15 @@
          let e2' = stripPLEUnfold e'
          let e3' = simplify γ ctx (eApps e2' es2)  -- reduces a bit the equations
 
-         if hasUndecidedGuard e' && guardOf e' == guardOf newE' then do
+         if hasUndecidedGuard e' && guardOf e' == guardOf newE' && et /= NoRWEta then do
            -- Don't unfold the expression if there is an if-then-else guarding
            -- it, just to preserve the size of further rewrites.
            -- If evalIte does any modifications, though, we do unfold in order
            -- to allow analysis of the resulting expression
+           -- Note(Alessio): this optimization make sense only if the
+           -- function is already fully applied in the original
+           -- program and not because of eta expansion, otherwise we might
+           -- miss redexes. See https://github.com/ucsd-progsys/liquidhaskell/issues/2652
            modify $ \st -> st
              { evPendingUnfoldings =
                  M.insertWith M.union (evExScope st) (M.singleton (eApps e0 es) e3') (evPendingUnfoldings st)
@@ -1132,10 +1144,17 @@
 evalApp γ ctx e0 es _et
   | eqs@(_:_) <- noUserDataMeasureEqs γ (eApps e0 es)
   = do
-       let eqs' = map (second $ simplify γ ctx) eqs
-       modify $ \st ->
-         st { evNewEqualities = foldr S.insert (evNewEqualities st) eqs' }
-       return Nothing
+       env <- gets (seSort . evEnv)
+       -- Only well-sorted LHSs should be considered. For instance, a measure
+       -- expecting an argument of type [[Int]] should not be applied to a value
+       -- of type [Int].
+       let eqs' = map (second $ simplify γ ctx) $
+                    filter (wellSorted env . fst) eqs
+       if null eqs' then return Nothing
+       else do
+         modify $ \st ->
+           st { evNewEqualities = foldr S.insert (evNewEqualities st) eqs' }
+         return Nothing
 
 evalApp γ ctx e0 es et
   | ELam (argName, _) body <- dropECst e0
@@ -1167,7 +1186,7 @@
         { evNewEqualities = S.insert (eApps e0 es, expandedTerm) (evNewEqualities st) }
       return (Just expandedTerm)
 
-evalApp _γ ctx e0 es _et
+evalApp γ ctx e0 es _et
   -- We check the annotation instead of the equations in γ for two reasons.
   --
   -- First, we want to eta expand functions that might not be reflected. Suppose
@@ -1202,6 +1221,15 @@
     -- is already handled by the previous case of evalApp
     modify $ \st -> st
       { evNewEqualities = S.insert (eApps e0 es, etaExpandedTerm) (evNewEqualities st) }
+
+    -- We also try to unfold the definition of the function in the eta
+    -- expanded body, as it might give us more information to generate
+    -- better equalities. Note that we pass NoRWEta to skip the optimization
+    redBody <- evalInExtendedEnv (zip etaNames etaArgsType) γ ctx NoRWEta fullBody
+    let etaExpandedRedBody = mkLams redBody (zip etaNames etaArgsType)
+    modify $ \st -> st
+      { evNewEqualities = S.insert (eApps e0 es, etaExpandedRedBody) (evNewEqualities st) }
+
     return (Just etaExpandedTerm)
   where
     unpackFFuncs (FFunc t ts) = t : unpackFFuncs ts
@@ -1237,6 +1265,10 @@
   , (rw, NoUserDataSMeasure) <- rws
   , length es == length (smArgs rw)
   ]
+
+-- | Check that an expression is well-sorted
+wellSorted :: SEnv Sort -> Expr -> Bool
+wellSorted env = Mb.isJust . checkSortExpr dummySpan env
 
 --------------------------------------------------------------------------------
 -- | 'substEq' unfolds or instantiates an equation at a particular list of
diff --git a/src/Language/Fixpoint/Solver/Prettify.hs b/src/Language/Fixpoint/Solver/Prettify.hs
--- a/src/Language/Fixpoint/Solver/Prettify.hs
+++ b/src/Language/Fixpoint/Solver/Prettify.hs
@@ -9,9 +9,10 @@
 import           Data.Bifunctor (first)
 import           Data.HashMap.Lazy (HashMap)
 import qualified Data.HashMap.Lazy as HashMap
+import qualified Data.HashMap.Strict as M
 import           Data.HashSet (HashSet)
 import qualified Data.HashSet as HashSet
-import           Data.List (intersperse, sortOn)
+import           Data.List (group, intersperse, sortOn)
 import           Data.Maybe (fromMaybe)
 import           Data.Text (Text)
 import qualified Data.Text as Text
@@ -38,9 +39,11 @@
   )
 import           Language.Fixpoint.Types.PrettyPrint
 import           Language.Fixpoint.Types.Refinements
-  ( ExprV(..)
+  ( ExprBV(..)
   , pattern PFalse
+  , pattern PKVar
   , Reft
+  , ReftBV(..)
   , SortedReft(..)
   , conjuncts
   , expr
@@ -72,6 +75,10 @@
   map
     (prettyConstraint (bs info) . snd)
     (sortOn fst $ HashMap.toList (cm info))
+  ++
+  map
+    (prettyWfConstraint (bs info) . snd)
+    (sortOn fst $ HashMap.toList (ws info))
 
 prettyConstraint
   :: Fixpoint a
@@ -130,6 +137,29 @@
       , sr_sort sr
       , reftPred $ sr_reft sr
       )
+
+prettyWfConstraint
+  :: Fixpoint a
+  => BindEnv a
+  -> WfC a
+  -> Doc
+prettyWfConstraint bindEnv wfc =
+  let prettyEnv =
+        concatMap (take 1) $
+        group $   -- eliminate duplicates
+        sortOn fst
+          [ (s, sr_sort sr)
+          | bId <- elemsIBindEnv $ wenv wfc
+          , let (s, sr, _a) = lookupBindEnv bId bindEnv
+          ]
+      (v, t, k) = wrft wfc
+   in hang (text "\n\nwf:") 2 $
+          hang (text "env:") 2
+            (vcat $ map prettyBind prettyEnv)
+      $+$ text "reft" <+> toFix (RR t (Reft (v, PKVar k M.empty mempty)))
+      $+$ toFixMeta (text "wf") (toFix (winfo wfc))
+  where
+    prettyBind (s, srt) = toFix s <+> ":" <+> toFix srt
 
 pprId :: Show a => Maybe a -> Doc
 pprId (Just i)  = "id" <+> text (show i)
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
@@ -189,7 +189,7 @@
 -- | `dropDeadSubsts` removes dead `K[x := e]` where `x` NOT in the domain of K.
 --------------------------------------------------------------------------------
 dropDeadSubsts :: F.SInfo a -> F.SInfo a
-dropDeadSubsts si = mapKVarSubsts (F.filterSubst . f) si
+dropDeadSubsts si = mapKVarSubsts (\k su -> F.toKVarSubst $ M.filterWithKey (f k) $ F.fromKVarSubst su) si
   where
     kvsM          = M.mapWithKey (\k _ -> kvDom k) (F.ws si)
     kvDom         = S.fromList . F.kvarDomain si
@@ -244,9 +244,9 @@
 badParams :: F.SInfo a -> F.SimpC a -> M.HashMap F.KVar [F.Symbol]
 badParams si c = Misc.group bads
   where
-    bads       = [ (k, x) | (v, k, F.Su su) <- subcKSubs xsrs c
+    bads       = [ (k, x) | (v, k, su) <- subcKSubs xsrs c
                           , let vEnv = maybe sEnv (`S.insert` sEnv) v
-                          , (x, e)          <- M.toList su
+                          , (x, e)          <- M.toList (F.fromKVarSubst su)
                           , badArg vEnv e
                  ]
     sEnv       = S.fromList (fst <$> xsrs)
@@ -256,16 +256,16 @@
 badArg sEnv (F.EVar y) = not (y `S.member` sEnv)
 badArg _    _          = True
 
-type KSub = (Maybe F.Symbol, F.KVar, F.Subst)
+type KSub = (Maybe F.Symbol, F.KVar, F.KVarSubst F.Symbol F.Symbol)
 
 subcKSubs :: [(F.Symbol, F.SortedReft)] -> F.SimpC a -> [KSub]
 subcKSubs xsrs c = rhs ++ lhs
   where
     lhs          = [ (Just v, k, su) | (_, sr) <- xsrs
                                      , let rs   = F.reftConjuncts (F.sr_reft sr)
-                                     , F.Reft (v, F.PKVar k su) <- rs
+                                     , F.Reft (v, F.PKVar k _ su) <- rs
                    ]
-    rhs          = [(Nothing, k, su) | F.PKVar k su <- [F.crhs c]]
+    rhs          = [(Nothing, k, su) | F.PKVar k _ su <- [F.crhs c]]
 
 
 initKvarEnv :: F.SInfo a -> KvDom
@@ -361,11 +361,11 @@
 --   it makes it hard to actually find the fundefs within (breaking PLE.)
 --------------------------------------------------------------------------------
 symbolEnv :: HasCallStack => Config -> F.SInfo a -> F.SymEnv
-symbolEnv cfg si = F.symEnv sEnv thyEnv ds lits (ts ++ ts')
+symbolEnv cfg si = F.symEnv cfg sEnv thyEnv ds lits (ts ++ ts')
   where
     ts'          = applySorts ae'
     ae'          = elaborate (ElabParam ef (F.atLoc E.dummySpan "symbolEnv") env0) (F.ae si)
-    env0         = F.symEnv sEnv thyEnv ds lits ts
+    env0         = F.symEnv cfg sEnv thyEnv ds lits ts
     thyEnv       = theoryEnv cfg si
     ds           = F.ddecls si
     ts           = Misc.setNub (applySorts si ++ [t | (_, t) <- F.toListSEnv sEnv])
diff --git a/src/Language/Fixpoint/Solver/Solution.hs b/src/Language/Fixpoint/Solver/Solution.hs
--- a/src/Language/Fixpoint/Solver/Solution.hs
+++ b/src/Language/Fixpoint/Solver/Solution.hs
@@ -14,29 +14,36 @@
     -- * Apply Solution
   , applyInSortedReft
   , CombinedEnv(..)
+  , qbPreds
 
     -- * Lookup Solution
   , lhsPred
 
   , nonCutsResult
 
+    -- * Save Solution
+  , saveSolution
+
     -- * Exported for Testing
   , simplifyKVar
   , alphaEq
   ) where
 
 import           Control.Arrow (second, (***))
-import           Control.Monad                  (guard, mplus)
+import           Control.Monad                  (guard, mplus, when)
 import           Control.Monad.Reader
 import qualified Data.HashSet                   as S
 import qualified Data.HashMap.Strict            as M
 import qualified Data.List                      as List
 import           Data.Maybe                     (maybeToList, isJust, isNothing)
+import qualified Text.PrettyPrint.HughesPJ      as PJ
 import           Language.Fixpoint.Types.PrettyPrint ()
 import           Language.Fixpoint.Types.Visitor      as V
 import           Language.Fixpoint.SortCheck          (ElabM)
 import qualified Language.Fixpoint.SortCheck          as So
+import           Language.Fixpoint.Misc               (ensurePath)
 import qualified Language.Fixpoint.Misc               as Misc
+import qualified Language.Fixpoint.Utils.Files        as Files
 import           Language.Fixpoint.Types.Config
 import qualified Language.Fixpoint.Types              as F
 import qualified Language.Fixpoint.Types.Solutions    as Sol
@@ -85,10 +92,11 @@
 --------------------------------------------------------------------------------
 
 refine :: F.SInfo a -> QCluster -> F.SEnv F.Sort -> F.WfC a -> ElabM Sol.QBind
-refine info qs genv w = refineK (allowHOquals info) env qs (F.wrft w)
+refine info qs genv w = refineK (allowHOquals info) env lits qs (F.wrft w)
   where
     env             = wenvSort <> genv
     wenvSort        = F.sr_sort <$> F.fromListSEnv (F.envCs (F.bs info) (F.wenv w))
+    lits            = getConstants info
 
 instConstants :: F.SInfo a -> F.SEnv F.Sort
 instConstants = F.fromListSEnv . filter notLit . F.toListSEnv . F.gLits
@@ -96,26 +104,43 @@
     notLit    = not . F.isLitSymbol . fst
 
 
-refineK :: Bool -> F.SEnv F.Sort -> QCluster -> (F.Symbol, F.Sort, F.KVar) -> ElabM Sol.QBind
-refineK ho env qs (v, t, _k) = Sol.qbFilterM (okInst env v t) eqs
+refineK :: Bool -> F.SEnv F.Sort -> [F.Constant] -> QCluster -> (F.Symbol, F.Sort, F.KVar) -> ElabM Sol.QBind
+refineK ho env lits qs (v, t, _k) = Sol.qbFilterM (okInst env v t) eqs
    where
-    eqs = instK ho env v t qs
+    eqs = instK ho env lits v t qs
 
 --------------------------------------------------------------------------------
 instK :: Bool
       -> F.SEnv F.Sort
+      -> [F.Constant]
       -> F.Symbol
       -> F.Sort
       -> QCluster
       -> Sol.QBind
 --------------------------------------------------------------------------------
-instK ho env v t qc = Sol.qb . unique $
-  [ Sol.eQual q xs
+instK ho env lits v t qc = Sol.qb . unique $
+  [ Sol.eQual q xs ls
       | (sig, qs) <- M.toList qc
-      , xs        <- instKSig ho env v t sig
+      , let (varSig, litSig) =  splitSig sig
+      , xs        <- instKSig ho env v t varSig
+      , ls        <- instLitSig lits litSig
       , q         <- qs
   ]
 
+-- split the QCSig into the parts that are for regular variables vs for wildcard-literals that are defined as `a#`, `b#` etc.
+-- e.g. see tests/horn/pos/wild_lits*.smt2
+splitSig :: QCSig -> (QCSig, QCSig)
+splitSig = List.partition (\qp -> qpPat qp /= PatLit)
+
+instLitSig :: [F.Constant] -> QCSig -> [[F.Constant]]
+instLitSig lits sig = sequence [ filter (matchSort (qpSort qp)) lits | qp <- sig ]
+
+matchSort :: F.Sort -> F.Constant -> Bool
+matchSort F.FInt  (F.I _)    = True
+matchSort F.FReal (F.R _)    = True
+matchSort s       (F.L _ s') = s == s'
+matchSort _       _          = False
+
 unique :: [Sol.EQual] -> [Sol.EQual]
 unique qs = M.elems $ M.fromList [ (Sol.eqPred q, q) | q <- qs ]
 
@@ -219,6 +244,7 @@
   F.PatSuffix i s -> JustSub i <$> F.stripSuffix s y
   F.PatNone       -> Just NoSub
   F.PatExact s    -> if s == y then Just NoSub else Nothing
+  F.PatLit        -> Nothing
   where
     y             =  F.unKArgSymbol y'
 
@@ -241,8 +267,7 @@
   where
     sr            = F.RR t (F.Reft (v, p))
     p             = Sol.eqPred eq
-
-    -- _msg          = printf "okInst: t = %s, eq = %s, env = %s" (F.showpp t) (F.showpp eq) (F.showpp env)
+    -- _msg          = printf "okInst: t = %s, eq = %s" (F.showpp t) (F.showpp eq)
 
 
 --------------------------------------------------------------------------------
@@ -328,13 +353,19 @@
 applyKVar :: Config -> CombinedEnv ann -> Sol.Sol Sol.QBind -> F.KVSub -> ExprInfo
 applyKVar cfg  g s ksu = case Sol.lookup s (F.ksuKVar ksu) of
   Left cs   -> hypPred cfg g s ksu cs
-  Right eqs -> let qbp = Sol.qbPreds (F.ksuSubst ksu) eqs
-                in (F.pAndNoDedup $ fst <$> qbp, mempty) -- TODO: don't initialize kvars that have a hyp solution
+  Right eqs -> let qbp = qbPreds
+                           (F.substFromKSubst $ F.ksuSubst ksu)
+                           (F.ksuTySub ksu)
+                           eqs
+                   preds = fst <$> qbp
+                in (F.pAndNoDedup preds, mempty) -- TODO: don't initialize kvars that have a hyp solution
 
+qbPreds :: F.Subst -> F.TyVarSubst -> Sol.QBind -> [(F.Pred, Sol.EQual)]
+qbPreds su tvsu (Sol.QB eqs) =
+  [ (F.subst su $ V.applyCoSub tvsu $ Sol.eqPred eq, eq) | eq <- eqs ]
+
 mkNonCutsExpr :: Config -> CombinedEnv ann -> Sol.Sol Sol.QBind -> F.KVar -> Sol.Hyp -> F.Expr
-mkNonCutsExpr cfg ce s k cs =
-  let bcps = map (bareCubePred cfg ce s k) cs
-   in F.pOr bcps
+mkNonCutsExpr cfg ce s k cs = F.pOr (bareCubePred cfg ce s k <$> cs)
 
 nonCutsResult :: Config -> F.BindEnv ann -> Sol.Sol Sol.QBind -> FixDelayedSolution
 nonCutsResult cfg be s = M.mapWithKey (\k -> Delayed . mkNonCutsExpr cfg g s k) $ Sol.sHyp s
@@ -368,11 +399,11 @@
         (p, _kI) = apply cfg g' s bs
      in F.pExist yts (p F.&.& psu)
   where
-    bs = Sol.cuBinds c
+    bs     = Sol.cuBinds c
     F.Su m = dropUnsortedExprs cfg g' (Sol.cuSubst c)
-    g' = addCEnv  g bs
-    bs' = F.diffIBindEnv bs (Misc.safeLookup "sScp" k (Sol.sScp s))
-    yts = symSorts g bs'
+    g'     = addCEnv  g bs
+    bs'    = F.diffIBindEnv bs (Misc.safeLookup "sScp" k (Sol.sScp s))
+    yts    = symSorts g bs'
 
 -- | At the moment, the liquid-fixpoint implementation allows for unsorted
 -- expressions in substitutions. See the discussion in
@@ -417,12 +448,14 @@
         -- Free variables in p should not colide with those generated by
         -- the rapier substitution. If that were the case, perhaps we would
         -- need to include @combinedSEnv g@ in the scope set.
-     in (F.rapierSubstExpr (F.substSymbolsSet su) su p, kI)
+        p' = F.rapierSubstExpr (F.substSymbolsSet su) su $
+             V.applyCoSub (F.ksuTySub ksu) p
+     in (p', kI)
   where
     bs' = F.diffIBindEnv bs (Misc.safeLookup "sScp" k (Sol.sScp s))
     bs  = Sol.cuBinds c
     k   = F.ksuKVar ksu
-    su = dropUnsortedExprs cfg g (F.ksuSubst  ksu)
+    su = dropUnsortedExprs cfg g (F.substFromKSubst $ F.ksuSubst  ksu)
 
 -- | @cubePredExc@ computes the predicate for the subset of binders bs'.
 --
@@ -644,3 +677,29 @@
     isVarIn (F.EVar s) vs
       | elem s vs = Just s
     isVarIn _ _vs = Nothing
+
+--------------------------------------------------------------------------------
+-- | Save Solution to File -----------------------------------------------------
+--------------------------------------------------------------------------------
+
+saveSolution :: Config -> String -> Result a -> IO ()
+saveSolution cfg sfx res = when (save cfg) $ do
+  let f = Files.tempFileName (srcFile cfg ++ sfx ++ ".fqout")
+  putStrLn $ "Saving Solution: " ++ f ++ "\n"
+  ensurePath f
+  writeFile f $ unlines $
+    [ ""
+    , "Solution:"
+    , scopedRender (resSolution  res)
+    ] ++
+    [ ""
+    , ""
+    , "Non-cut kvars:"
+    , ""
+    , scopedRender (M.map forceDelayed $ resNonCutsSolution res)
+    ]
+    where
+      scopedRender = PJ.render . PJ.vcat . map ncDoc . scoped
+      scoped sol = [ (k, scope k, So.unApply e) | (k, e) <- M.toList sol]
+      scope k = M.lookupDefault [] k $ resSorts res
+      ncDoc (k, xts, e) = PJ.hsep [ F.pprint k PJ.<> F.pprint xts, PJ.text ":=", F.pprint e ]
diff --git a/src/Language/Fixpoint/Solver/Solve.hs b/src/Language/Fixpoint/Solver/Solve.hs
--- a/src/Language/Fixpoint/Solver/Solve.hs
+++ b/src/Language/Fixpoint/Solver/Solve.hs
@@ -153,6 +153,8 @@
 
   res2  <- case resStatus res1 of  {- then run normal PLE on remaining unsolved constraints -}
     Unsafe _ bads2 | rewriteAxioms cfg -> do
+      when (save cfg) $
+        liftIO $ S.saveSolution cfg ".pre-ple" res1
       liftSMT $ smtComment "solve: ple"
       bs <- liftSMT $ PLE.instantiate cfg fi1 (Just s3) (Just $ map fst bads2)
       -- Check the constraints one last time after PLE
@@ -268,12 +270,12 @@
     rhsCands s = M.toList $ M.fromList $ map cnd ks
       where
         ks          = predKs . F.crhs $ c
-        cnd :: (F.KVar, F.Subst) -> (F.KVar , Sol.Cand Sol.EQual)
-        cnd (k, su) = (k, Sol.qbPreds su (Sol.lookupQBind s k))
+        cnd :: (F.KVar, F.Subst, F.TyVarSubst) -> (F.KVar , Sol.Cand Sol.EQual)
+        cnd (k, su, tvsu) = (k, S.qbPreds su tvsu (Sol.lookupQBind s k))
 
-predKs :: F.Expr -> [(F.KVar, F.Subst)]
+predKs :: F.Expr -> [(F.KVar, F.Subst, F.TyVarSubst)]
 predKs (F.PAnd ps)    = concatMap predKs ps
-predKs (F.PKVar k su) = [(k, su)]
+predKs (F.PKVar k tvsu su) = [(k, F.substFromKSubst su, tvsu)]
 predKs _              = []
 
 --------------------------------------------------------------------------------
diff --git a/src/Language/Fixpoint/Solver/UniqifyKVars.hs b/src/Language/Fixpoint/Solver/UniqifyKVars.hs
--- a/src/Language/Fixpoint/Solver/UniqifyKVars.hs
+++ b/src/Language/Fixpoint/Solver/UniqifyKVars.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE CPP                    #-}
+{-# LANGUAGE ViewPatterns           #-}
 {-# OPTIONS_GHC -Wno-name-shadowing #-}
 
 {- | This module creates new bindings for each argument of each kvar.
@@ -56,14 +57,14 @@
 --------------------------------------------------------------------------------
 remakeSubsts fi = mapKVarSubsts (remakeSubst fi) fi
 
-remakeSubst :: SInfo a -> KVar -> Subst -> Subst
+remakeSubst :: SInfo a -> KVar -> KVarSubst Symbol Symbol -> KVarSubst Symbol Symbol
 remakeSubst fi k su = foldl' (updateSubst k) su (kvarDomain fi k)
 
-updateSubst :: KVar -> Subst -> Symbol -> Subst
-updateSubst k (Su su) sym
+updateSubst :: KVar -> KVarSubst Symbol Symbol -> Symbol -> KVarSubst Symbol Symbol
+updateSubst k (fromKVarSubst -> su) sym
   = case M.lookup sym su of
-      Just z  -> Su $ M.delete sym $ M.insert ksym z          su
-      Nothing -> Su $                M.insert ksym (eVar sym) su
+      Just z  -> toKVarSubst $ M.delete sym $ M.insert ksym z          su
+      Nothing -> toKVarSubst $                M.insert ksym (eVar sym) su
     where
       kx      = kv k
       ksym    = kArgSymbol sym kx
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
@@ -8,6 +8,7 @@
 {-# LANGUAGE PatternGuards         #-}
 {-# LANGUAGE BangPatterns          #-}
 {-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE TypeOperators         #-}
 {-# LANGUAGE InstanceSigs #-}
 
 -- | This module has the functions that perform sort-checking, and related
@@ -206,14 +207,14 @@
 
 elaborateExpr :: HasCallStack => ElabParam -> Expr -> Maybe Sort -> Expr
 elaborateExpr (ElabParam ef msg env) e t =
-  elabNumeric . elabApply env' . elabExpr (ElabParam ef msg env') t .  elabSorts ef . elabFMap . (if Cfg.elabSetBag ef then elabFSetBagZ3 else id) $ e
+  elabNumeric env' . elabApply env' . elabExpr (ElabParam ef msg env') t .  elabSorts ef . elabFMap . (if Cfg.elabSetBag ef then elabFSetBagZ3 else id) $ e
     where
       env' = coerceEnv ef env
 
 skipElabExpr :: ElabParam -> Expr -> Expr
 skipElabExpr ep e = case elabExprE ep Nothing e of
   Left _   -> e
-  Right e' -> elabNumeric . elabApply (epEnv ep) $ e'
+  Right e' -> elabNumeric (epEnv ep) . elabApply (epEnv ep) $ e'
 
 instance Elaborate (Symbol, Sort) where
   elaborate ep (x, s) = (x, elaborate ep s)
@@ -221,17 +222,17 @@
 instance Elaborate a => Elaborate [a]  where
   elaborate ep xs = elaborate ep <$> xs
 
-elabNumeric :: Expr -> Expr
-elabNumeric = Vis.mapExprOnExpr go
+elabNumeric :: SymEnv -> Expr -> Expr
+elabNumeric env = Vis.mapExprOnExpr go
   where
     go (ETimes e1 e2)
-      | exprSort "txn1" e1 == FReal
-      , exprSort "txn2" e2 == FReal
+      | isFractional env (exprSort ("txn3: " ++ showpp e1) e1)
+      , isFractional env (exprSort "txn4" e2)
       = ERTimes e1 e2
     go (EDiv   e1 e2)
-      | exprSort ("txn3: " ++ showpp e1) e1 == FReal
-      , exprSort "txn4" e2 == FReal
-      = ERDiv   e1 e2
+      | isFractional env (exprSort ("txn3: " ++ showpp e1) e1)
+      , isFractional env (exprSort "txn4" e2)
+      = ERDiv e1 e2
     go e
       = e
 
@@ -286,7 +287,7 @@
 elabFMap (PAll   bs e)     = PAll bs (elabFMap e)
 elabFMap (PExist bs e)     = PExist bs (elabFMap e)
 elabFMap (ECoerc a t e)    = ECoerc a t (elabFMap e)
-elabFMap (PKVar k (Su m))  = PKVar k (Su (elabFMap <$> m))
+elabFMap (PKVar k tsu su)      = PKVar k tsu (mapKVarSubst elabFMap su)
 elabFMap e                 = e
 
 
@@ -333,7 +334,7 @@
     go (PAll   bs e)      = PAll bs (go e)
     go (PExist bs e)      = PExist bs (go e)
     go (ECoerc a t e)     = ECoerc a t (go e)
-    go (PKVar k (Su m))   = PKVar k (Su (go <$> m))
+    go (PKVar k tsu su)       = PKVar k tsu (mapKVarSubst go su)
     go e                  = e
 
 -- | Reverse transformation of elabFSetBagZ3: converts array representations back to set/bag operations
@@ -412,7 +413,7 @@
     go (PAll   bs e)      = PAll bs (go e)
     go (PExist bs e)      = PExist bs (go e)
     go (ECoerc a t e)     = ECoerc a t (go e)
-    go (PKVar k (Su m))   = PKVar k (Su (go <$> m))
+    go (PKVar k tsu su)       = PKVar k tsu (mapKVarSubst go su)
     go e                  = e
 
 
@@ -435,7 +436,7 @@
 elabSorts ef (PAll   bs e)     = PAll bs (elabSorts ef e)
 elabSorts ef (PExist bs e)     = PExist bs (elabSorts ef e)
 elabSorts ef (ECoerc s1 s2 e)  = ECoerc (coerceSort ef s1) (coerceSort ef s2) (elabSorts ef e)
-elabSorts ef (PKVar k (Su m))  = PKVar k (Su (elabSorts ef <$> m))
+elabSorts ef (PKVar k tsu su)      = PKVar k tsu (mapKVarSubst (elabSorts ef) su)
 elabSorts _ e                 = e
 
 --------------------------------------------------------------------------------
@@ -502,7 +503,7 @@
     step e@EApp {}        = go e
     step (ELam b e)       = ELam b       (go e)
     step (ECoerc a t e)   = ECoerc a t   (go e)
-    step (PKVar k (Su m)) = PKVar k (Su (go <$> m))
+    step (PKVar k tsu su)     = PKVar k tsu (mapKVarSubst go su)
     step e@ESym{}         = e
     step e@ECon{}         = e
     step e@EVar{}         = e
@@ -535,7 +536,7 @@
             Just z  -> Found z
             Nothing -> Alts []
 
-subEnv :: (Subable e) => SEnv a -> e -> SEnv a
+subEnv :: (Subable e, Variable e ~ Symbol) => SEnv a -> e -> SEnv a
 subEnv g e = intersectWithSEnv const g g'
   where
     g' = fromListSEnv $ (, ()) <$> syms e
@@ -759,14 +760,14 @@
 -- TODO: the guard below is because some LH tests generate PKVar with ill-sorted substitutions.
 -- However, a cleaner solution could be to modify `Sanitize.restrictKVarDomain` to simply
 -- those ill-sorted substitutions right up at the outset.
-elab !f e@(PKVar k (Su m)) = do
+elab !f e@(PKVar k tsu su) = do
   expKvars <- asks (elabExplicitKvars . chElabF)
   if expKvars
     then do
-      xargs' <- forM (HashMap.toList m) $ \(x, arg) -> do
+      xargs' <- forM (HashMap.toList $ fromKVarSubst su) $ \(x, arg) -> do
         (arg', _) <- elab f arg
         return (x, arg')
-      return (PKVar k (Su (HashMap.fromList xargs')), boolSort)
+      return (PKVar k tsu (toKVarSubst (HashMap.fromList xargs')), boolSort)
     else
       return (e, boolSort)
 
@@ -972,6 +973,13 @@
   SReal   -> True
   _       -> False
 
+isFractional :: SymEnv -> Sort -> Bool
+isFractional env (FObj l)
+  = lookupSEnv l (seSort env) `elem` [Just FFrac, Just realSort]
+isFractional _ s = isReal s
+
+
+
 toIntAt :: Sort -> Expr
 toIntAt s = ECst (EVar toIntName) (FFunc s FInt)
 
@@ -1299,7 +1307,7 @@
 checkFractional :: Env -> Sort -> CheckM ()
 checkFractional f s@(FObj l)
   = do t <- checkSym f l
-       unless (t == FFrac) $ throwErrorAt (errNonFractional s)
+       unless (t `elem` [FFrac, realSort]) (throwErrorAt $ errNonFractional s)
 checkFractional _ s
   = unless (isReal s) $ throwErrorAt (errNonFractional s)
 
@@ -1499,6 +1507,14 @@
   checkNumeric f t `withError` errUnify e FInt t
   return θ
 
+unify1 f e !θ !t FReal = do
+  checkFractional f t `withError` errUnify e t FReal
+  return θ
+
+unify1 f e !θ FReal !t = do
+  checkFractional f t `withError` errUnify e FReal t
+  return θ
+
 unify1 f e !θ (FFunc !t1 !t2) (FFunc !t1' !t2') =
   unifyMany f e θ [t1, t2] [t1', t2']
 
@@ -1601,16 +1617,6 @@
   where
     f (ECst !e' !s) = ECst e' (apply θ s)
     f !e'          = e'
-
---------------------------------------------------------------------------------
-_applyCoercion :: Symbol -> Sort -> Sort -> Sort
---------------------------------------------------------------------------------
-_applyCoercion a t = Vis.mapSort f
-  where
-    f (FObj b)
-      | a == b    = t
-    f s           = s
-
 
 --------------------------------------------------------------------------------
 -- | Deconstruct a function-sort -----------------------------------------------
diff --git a/src/Language/Fixpoint/Types.hs b/src/Language/Fixpoint/Types.hs
--- a/src/Language/Fixpoint/Types.hs
+++ b/src/Language/Fixpoint/Types.hs
@@ -5,7 +5,7 @@
 
 module Language.Fixpoint.Types (module X) where
 
-import Language.Fixpoint.Types.SMTPrint      as X
+import Language.Fixpoint.Types.SMTPrint         as X
 import Language.Fixpoint.Types.PrettyPrint      as X
 import Language.Fixpoint.Types.Names            as X
 import Language.Fixpoint.Types.Errors           as X
@@ -19,3 +19,4 @@
 import Language.Fixpoint.Types.Triggers         as X
 import Language.Fixpoint.Types.Theories         as X
 import Language.Fixpoint.Types.Templates        as X
+import Language.Fixpoint.Types.Binders          as X
diff --git a/src/Language/Fixpoint/Types/Binders.hs b/src/Language/Fixpoint/Types/Binders.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Fixpoint/Types/Binders.hs
@@ -0,0 +1,10 @@
+module Language.Fixpoint.Types.Binders where
+
+import Data.Hashable (Hashable)
+
+class (Eq b, Ord b, Hashable b) => Binder b where
+  wildcard :: b
+  editDistance :: b -> b -> Int
+  editDistance b1 b2
+    | b1 == b2  = 0
+    | otherwise = maxBound
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
@@ -103,6 +103,7 @@
   , pleUndecGuards   :: Bool           -- ^ Unfold invocations with undecided guards in PLE
   , etabeta          :: Bool           -- ^ Eta expand and beta reduce terms to aid PLE
   , localRewrites    :: Bool           -- ^ Eta expand and beta reduce terms to aid PLE
+  , saveBfqOnError   :: Bool           -- ^ save FInfo as .bfq only on verification failure
   , interpreter      :: Bool           -- ^ Do not use the interpreter to assist PLE
   , noEnvReduction   :: Bool     -- ^ Don't use environment reduction
   , inlineANFBinds   :: Bool          -- ^ Inline ANF bindings.
@@ -117,6 +118,7 @@
   , noStringTheory :: Bool             -- ^ disable interpretation of string theory by SMT
   , explicitKvars  :: Bool             -- ^ use explicitly declared kvars (horn style) which disables several "defensive simplifications"
   , sortedSolution :: Bool             -- ^ leave sorts in the solution
+  , saveDir        :: Maybe FilePath    -- ^ output directory for --save generated files (default: .liquid/ next to source)
   } deriving (Eq,Data,Typeable,Show,Generic)
 
 instance Default Config where
@@ -248,6 +250,15 @@
   , elimStats                = False   &= help "(alpha) Print eliminate stats"
   , solverStats              = False   &= help "Print solver stats"
   , save                     = False   &= help "Save Query as .fq and .bfq files"
+  , saveBfqOnError           = False   &= help "Save Query as .bfq file only when verification fails"
+                                       &= name "save-bfq-on-error"
+                                       &= explicit
+  , saveDir                  = Nothing
+      &= name "save-dir"
+      &= help "Output directory for --save generated files (default: .liquid/ next to source)"
+      &= opt (Nothing :: Maybe FilePath)
+      &= explicit
+      &= typDir
   , metadata                 = False   &= help "Print meta-data associated with constraints"
   , stats                    = False   &= help "Compute constraint statistics"
   , etaElim                  = False   &= help "Eta elimination in function definition"
@@ -322,4 +333,4 @@
 multicore cfg = cores cfg /= Just 1
 
 queryFile :: Ext -> Config -> FilePath
-queryFile e = extFileName e . srcFile
+queryFile e cfg = extFileNameR' (saveDir cfg) e (srcFile cfg)
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
@@ -28,6 +28,7 @@
   , toFixpoint
   , writeFInfo
   , saveQuery
+  , saveBinaryQuery
   , saveSInfo
 
    -- * Constructing Queries
@@ -121,7 +122,7 @@
 import           Language.Fixpoint.Types.Spans
 import           Language.Fixpoint.Types.Sorts
 import           Language.Fixpoint.Types.Refinements
-import           Language.Fixpoint.Types.Substitutions
+import           Language.Fixpoint.Types.Substitutions()
 import           Language.Fixpoint.Types.Environments
 import qualified Language.Fixpoint.Utils.Files as Files
 import qualified Language.Fixpoint.Solver.Stats as Solver
@@ -393,7 +394,7 @@
   toFix w     = hang (text "\n\nwf:") 2 bd
     where bd  =   toFix (wenv w)
               -- NOTE: this next line is printed this way for compatability with the OCAML solver
-              $+$ text "reft" <+> toFix (RR t (Reft (v, PKVar k mempty)))
+              $+$ text "reft" <+> toFix (RR t (Reft (v, PKVar k M.empty mempty)))
               $+$ toFixMeta (text "wf") (toFix (winfo w))
           (v, t, k) = wrft w
 
@@ -442,7 +443,7 @@
 ---------------------------------------------------------------------------
 
 wfC :: (Fixpoint a) => IBindEnv -> SortedReft -> a -> [WfC a]
-wfC be sr x = if all isEmptySubst sus -- ++ gsus)
+wfC be sr x = if all isEmptyKVarSubst sus -- ++ gsus)
                  -- NV TO RJ This tests fails with [LT:=GHC.Types.LT][EQ:=GHC.Types.EQ][GT:=GHC.Types.GT]]
                  -- NV TO RJ looks like a resolution issue
                 then [WfC be (v, sr_sort sr, k) x      | k         <- ks ]
@@ -452,10 +453,11 @@
     Reft (v, ras)   = sr_reft sr
     (ks, sus)       = unzip $ go ras
 
-    go (PKVar k su) = [(k, su)]
-    go (PAnd es)    = [(k, su) | PKVar k su <- es]
+    go (PKVar k _ su) = [(k, su)]
+    go (PAnd es)    = [(k, su) | PKVar k _ su <- es]
     go _            = []
 
+
 mkSubC :: IBindEnv -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a
 mkSubC = SubC
 
@@ -514,6 +516,7 @@
   | PatPrefix !Symbol !Int  -- ^ str . $i  i.e. match prefix 'str' with suffix bound to $i
   | PatSuffix !Int !Symbol  -- ^ $i . str  i.e. match suffix 'str' with prefix bound to $i
   | PatExact  !Symbol       -- ^ str       i.e. exactly match 'str'
+  | PatLit                  -- ^ match literals of the given sort
   deriving (Eq, Ord, Show, Data, Typeable, Generic)
 
 instance ToJSON   Qualifier   where
@@ -566,6 +569,7 @@
   pprintTidy k (PatPrefix s i) = "as" <+> pprintTidy k s <+> ("$" <-> pprint i)
   pprintTidy k (PatSuffix s i) = "as" <+> ("$" <-> pprint i) <+> pprintTidy k s
   pprintTidy k (PatExact  s  ) = "~"  <+> pprintTidy k s
+  pprintTidy _ PatLit          = "as lit"
 
 instance Fixpoint Qualifier where
   toFix = pprQual
@@ -1059,29 +1063,28 @@
 
 instance Hashable AutoRewrite
 
-
-instance Fixpoint (M.HashMap SubcId [AutoRewrite]) where
-  toFix autoRW =
-    vcat $
-    map fixRW rewrites ++
-    rwsMapping
-    where
-      rewrites = dedupAutoRewrites autoRW
+autoRWToFix :: M.HashMap SubcId [AutoRewrite] -> Doc
+autoRWToFix autoRW =
+  vcat $
+  map fixRW rewrites ++
+  rwsMapping
+  where
+    rewrites = dedupAutoRewrites autoRW
 
-      fixRW rw@(AutoRewrite args lhs rhs) =
-          text ("autorewrite " ++ show (hash rw))
-          <+> hsep (map toFix args)
-          <+> text "="
-          <+> text "{"
-          <+> toFix lhs
-          <+> text "="
-          <+> toFix rhs
-          <+> text "}"
+    fixRW rw@(AutoRewrite args lhs rhs) =
+        text ("autorewrite " ++ show (hash rw))
+        <+> hsep (map toFix args)
+        <+> text "="
+        <+> text "{"
+        <+> toFix lhs
+        <+> text "="
+        <+> toFix rhs
+        <+> text "}"
 
-      rwsMapping = do
-        (cid, rws) <- M.toList autoRW
-        rw         <-  rws
-        return $ "rewrite" <+> brackets (text $ show cid ++ " : " ++ show (hash rw))
+    rwsMapping = do
+      (cid, rws) <- M.toList autoRW
+      rw         <-  rws
+      return $ "rewrite" <+> brackets (text $ show cid ++ " : " ++ show (hash rw))
 
 
 
@@ -1103,7 +1106,7 @@
 instance Fixpoint AxiomEnv where
   toFix axe = vcat ((toFix <$> L.sort (aenvEqs axe)) ++ (toFix <$> L.sort (aenvSimpl axe)))
               $+$ renderExpand (pairdoc <$> L.sort (M.toList $ aenvExpand axe))
-              $+$ toFix (aenvAutoRW axe)
+              $+$ autoRWToFix (aenvAutoRW axe)
     where
       pairdoc (x,y) = text $ show x ++ " : " ++ show y
       renderExpand [] = empty
diff --git a/src/Language/Fixpoint/Types/Environments.hs b/src/Language/Fixpoint/Types/Environments.hs
--- a/src/Language/Fixpoint/Types/Environments.hs
+++ b/src/Language/Fixpoint/Types/Environments.hs
@@ -14,8 +14,10 @@
 module Language.Fixpoint.Types.Environments (
 
   -- * Environments
-    SEnv(..)
-  , SESearch(..)
+    SEnv
+  , SEnvB(..)
+  , SESearch
+  , SESearchB(..)
   , emptySEnv, toListSEnv, fromListSEnv, fromMapSEnv
   , mapSEnvWithKey, mapSEnv, mapMSEnv
   , insertSEnv, deleteSEnv, memberSEnv, lookupSEnv, unionSEnv, unionSEnv'
@@ -66,6 +68,7 @@
 import           Data.Generics             (Data)
 import           Data.Typeable             (Typeable)
 import           GHC.Generics              (Generic)
+import           Data.Hashable             (Hashable)
 import qualified Data.HashMap.Strict       as M
 import qualified Data.HashSet              as S
 import           Data.Maybe
@@ -75,6 +78,7 @@
 
 import           Language.Fixpoint.Types.Config
 import           Language.Fixpoint.Types.PrettyPrint
+import           Language.Fixpoint.Types.Binders
 import           Language.Fixpoint.Types.Names
 import           Language.Fixpoint.Types.Sorts
 import           Language.Fixpoint.Types.Refinements
@@ -89,8 +93,9 @@
 instance PPrint IBindEnv where
   pprintTidy _ = pprint . L.sort . elemsIBindEnv
 
-newtype SEnv a     = SE { seBinds :: M.HashMap Symbol a }
-                     deriving (Eq, Data, Typeable, Generic, Foldable, Traversable)
+type SEnv a = SEnvB Symbol a
+newtype SEnvB b a = SE { seBinds :: M.HashMap b a }
+                    deriving (Eq, Data, Typeable, Generic, Foldable, Traversable)
 
 data SizedEnv a    = BE { _beSize  :: !Int
                         , beBinds :: !(BindMap a)
@@ -111,74 +116,74 @@
 -- data SolEnv        = SolEnv { soeBinds :: !BindEnv }
 --                     deriving (Eq, Show, Generic)
 
-instance PPrint a => PPrint (SEnv a) where
+instance (Ord b, PPrint b, PPrint a) => PPrint (SEnvB b a) where
   pprintTidy k = pprintKVs k . L.sortBy (compare `on` fst) . toListSEnv
 
 {-# SCC toListSEnv #-}
-toListSEnv              ::  SEnv a -> [(Symbol, a)]
+toListSEnv              ::  SEnvB b a -> [(b, a)]
 toListSEnv (SE env)     = M.toList env
 
-fromListSEnv            ::  [(Symbol, a)] -> SEnv a
+fromListSEnv            ::  Hashable b => [(b, a)] -> SEnvB b a
 fromListSEnv            = SE . M.fromList
 
-fromMapSEnv             ::  M.HashMap Symbol a -> SEnv a
+fromMapSEnv             ::  M.HashMap b a -> SEnvB b a
 fromMapSEnv             = SE
 
-mapSEnv                 :: (a -> b) -> SEnv a -> SEnv b
+mapSEnv                 :: (a₁ -> a₂) -> SEnvB b a₁ -> SEnvB b a₂
 mapSEnv f (SE env)      = SE (fmap f env)
 
-mapMSEnv                :: (Monad m) => (a -> m b) -> SEnv a -> m (SEnv b)
+mapMSEnv                :: (Monad m, Hashable b) => (a₁ -> m a₂) -> SEnvB b a₁ -> m (SEnvB b a₂)
 mapMSEnv f env          = fromListSEnv <$> mapM (secondM f) (toListSEnv env)
 
-mapSEnvWithKey          :: ((Symbol, a) -> (Symbol, b)) -> SEnv a -> SEnv b
+mapSEnvWithKey          :: Hashable b => ((b, a₁) -> (b, a₂)) -> SEnvB b a₁ -> SEnvB b a₂
 mapSEnvWithKey f        = fromListSEnv . fmap f . toListSEnv
 
-deleteSEnv :: Symbol -> SEnv a -> SEnv a
+deleteSEnv :: Hashable b => b -> SEnvB b a -> SEnvB b a
 deleteSEnv x (SE env)   = SE (M.delete x env)
 
-insertSEnv :: Symbol -> a -> SEnv a -> SEnv a
+insertSEnv :: Hashable b => b -> a -> SEnvB b a -> SEnvB b a
 insertSEnv x v (SE env) = SE (M.insert x v env)
 
 {-# SCC lookupSEnv #-}
-lookupSEnv :: Symbol -> SEnv a -> Maybe a
+lookupSEnv :: Hashable b => b -> SEnvB b a -> Maybe a
 lookupSEnv x (SE env)   = M.lookup x env
 
-emptySEnv :: SEnv a
+emptySEnv :: SEnvB b a
 emptySEnv               = SE M.empty
 
-memberSEnv :: Symbol -> SEnv a -> Bool
+memberSEnv :: Hashable b => b -> SEnvB b a -> Bool
 memberSEnv x (SE env)   = M.member x env
 
-intersectWithSEnv :: (v1 -> v2 -> a) -> SEnv v1 -> SEnv v2 -> SEnv a
+intersectWithSEnv :: Eq b => (a₁ -> a₂ -> a) -> SEnvB b a₁ -> SEnvB b a₂ -> SEnvB b a
 intersectWithSEnv f (SE m1) (SE m2) = SE (M.intersectionWith f m1 m2)
 
-differenceSEnv :: SEnv a -> SEnv w -> SEnv a
+differenceSEnv :: Hashable b => SEnvB b a -> SEnvB b w -> SEnvB b a
 differenceSEnv (SE m1) (SE m2) = SE (M.difference m1 m2)
 
-filterSEnv :: (a -> Bool) -> SEnv a -> SEnv a
+filterSEnv :: (a -> Bool) -> SEnvB b a -> SEnvB b a
 filterSEnv f (SE m)     = SE (M.filter f m)
 
-unionSEnv :: SEnv a -> M.HashMap Symbol a -> SEnv a
+unionSEnv :: Eq b => SEnvB b a -> M.HashMap b a -> SEnvB b a
 unionSEnv (SE m1) m2    = SE (M.union m1 m2)
 
-unionSEnv' :: SEnv a -> SEnv a -> SEnv a
+unionSEnv' :: Eq b => SEnvB b a -> SEnvB b a -> SEnvB b a
 unionSEnv' (SE m1) (SE m2)    = SE (M.union m1 m2)
 
 {-# SCC lookupSEnvWithDistance #-}
-lookupSEnvWithDistance :: Symbol -> SEnv a -> SESearch a
+lookupSEnvWithDistance :: Binder b => b -> SEnvB b a -> SESearchB b a
 lookupSEnvWithDistance x (SE env)
   = case M.lookup x env of
      Just z  -> Found z
-     Nothing -> Alts $ symbol <$> alts
+     Nothing -> Alts alts
   where
-    alts       = takeMin $ zip (editDistance x' <$> ss) ss
-    ss         = symbolString . fst <$> M.toList env
-    x'         = symbolString x
+    alts       = takeMin $ zip (editDistance x <$> ss) ss
+    ss         = fst <$> M.toList env
     takeMin xs = [z | (d, z) <- xs, d == getMin xs]
     getMin     = minimum . (fst <$>)
 
 
-data SESearch a = Found a | Alts [Symbol]
+type SESearch a = SESearchB Symbol a
+data SESearchB b a = Found a | Alts [b]
   deriving Show
 
 -- | Functions for Indexed Bind Environment
@@ -283,7 +288,7 @@
 deleteBindEnv :: BindId -> BindEnv a -> BindEnv a
 deleteBindEnv i (BE n m) = BE n $ M.delete i m
 
-instance Functor SEnv where
+instance Functor (SEnvB b) where
   fmap = mapSEnv
 
 instance Fixpoint (EBindEnv a) where
@@ -302,10 +307,10 @@
 instance Fixpoint (SEnv a) => Show (SEnv a) where
   show = render . toFix
 
-instance Semigroup (SEnv a) where
+instance Eq b => Semigroup (SEnvB b a) where
   s1 <> s2 = SE $ M.union (seBinds s1) (seBinds s2)
 
-instance Monoid (SEnv a) where
+instance Eq b => Monoid (SEnvB b a) where
   mempty        = SE M.empty
 
 instance Semigroup (BindEnv a) where
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
@@ -148,6 +148,8 @@
 import qualified GHC.Arr                     as Arr
 import           GHC.Generics                (Generic)
 import           Text.PrettyPrint.HughesPJ   (text)
+import           Language.Fixpoint.Misc
+import           Language.Fixpoint.Types.Binders
 import           Language.Fixpoint.Types.PrettyPrint
 import           Language.Fixpoint.Types.Spans
 import           Language.Fixpoint.Utils.Builder as Builder (fromText)
@@ -209,6 +211,10 @@
   -- NOTE: hash based on original text rather than id
   hashWithSalt s (S _ t _) = hashWithSalt s t
 
+instance Binder Symbol where
+  wildcard = vv Nothing
+  editDistance s1 s2 = levenshteinDistance (symbolString s1) (symbolString s2)
+
 instance NFData Symbol where
   rnf S {} = ()
 
@@ -256,7 +262,7 @@
   toFix = text . T.unpack
 
 {- | [NOTE: SymbolText]
-	Use `symbolSafeText` if you want it to machine-readable,
+        Use `symbolSafeText` if you want it to machine-readable,
         but `symbolText`     if you want it to be human-readable.
  -}
 
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
@@ -31,6 +31,12 @@
   toFix xs = brackets $ sep $ punctuate ";" (toFix <$> L.sort (S.toList xs))
   simplify = S.fromList . map simplify . S.toList
 
+instance (Ord k, Hashable k, Fixpoint k, Fixpoint v) => Fixpoint (M.HashMap k v) where
+  toFix m = case hashMapToAscList m of
+              []  -> empty
+              xys -> hcat $ map (\(x,y) -> brackets $ toFix x <-> text ":=" <-> toFix y) xys
+  simplify = M.map simplify . M.mapKeys simplify
+
 instance Fixpoint () where
   toFix _ = "()"
 
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
@@ -14,6 +14,7 @@
 {-# LANGUAGE GADTs                      #-}
 {-# LANGUAGE PatternSynonyms            #-}
 {-# LANGUAGE ViewPatterns               #-}
+{-# LANGUAGE TypeFamilies               #-}
 
 {-# OPTIONS_GHC -Wno-orphans            #-}
 
@@ -26,7 +27,8 @@
   , Constant (..)
   , Bop (..)
   , Brel (..)
-  , ExprV (..), Pred
+  , ExprBV (..)
+  , ExprV, Pred
   , Expr
   , pattern PTrue, pattern PTop, pattern PFalse, pattern EBot
   , pattern ETimes, pattern ERTimes, pattern EDiv, pattern ERDiv
@@ -34,10 +36,13 @@
   , KVar (..)
   , Subst
   , SubstV (..)
+  , KVarSubst
   , KVSub (..)
   , Reft
-  , ReftV (..)
+  , ReftV
+  , ReftBV (..)
   , SortedReft (..)
+  , TyVarSubst
 
   -- * Constructing Terms
   , eVar, elit
@@ -68,6 +73,7 @@
   , predReft                -- any pred : p
   , reftPred
   , reftBind
+  , toKVarSubst
 
   -- * Predicates
   , isFunctionSortedReft, functionSort
@@ -95,18 +101,24 @@
   , sortedReftSymbols
   , substSortInExpr
   , sortSubstInExpr
+  , fromKVarSubst
+  , isEmptyKVarSubst
 
   -- * Transforming
   , mapPredReft
   , onEverySubexpr
+  , mapBindExpr
   , pprintReft
+  , mapKVarSubst
+  , mapBindKVarSubst
+  , mapBindReft
 
   , debruijnIndex
 
   ) where
 
 import           Prelude hiding ((<>))
-import           Data.Bifunctor (second)
+import           Data.Bifunctor (first, second)
 import qualified Data.Store as S
 import           Data.Generics             (Data, gmapT, mkT, extT)
 import           Data.Typeable             (Typeable)
@@ -130,6 +142,7 @@
 import           Control.DeepSeq
 import           Data.Maybe                (isJust)
 import           Language.Fixpoint.Types.Names
+import           Language.Fixpoint.Types.Binders
 import           Language.Fixpoint.Types.PrettyPrint
 import           Language.Fixpoint.Types.Spans
 import           Language.Fixpoint.Types.Sorts
@@ -147,7 +160,8 @@
 instance NFData SymConst
 instance NFData Brel
 instance NFData Bop
-instance NFData v => NFData (ExprV v)
+instance (NFData b, NFData v) => NFData (KVarSubst b v)
+instance (NFData b, NFData v) => NFData (ExprBV b v)
 instance NFData v => NFData (ReftV v)
 instance NFData SortedReft
 
@@ -161,6 +175,7 @@
 instance S.Store SymConst
 instance S.Store Brel
 instance S.Store Bop
+instance S.Store (KVarSubst Symbol Symbol)
 instance S.Store Expr
 instance S.Store Reft
 instance S.Store SortedReft
@@ -177,8 +192,9 @@
   put = B.put . M.toList
   get = M.fromList <$> B.get
 
-instance B.Binary v => B.Binary (SubstV v)
-instance B.Binary v => B.Binary (ExprV v)
+instance (B.Binary v, Hashable v) => B.Binary (SubstV v)
+instance (B.Binary b, B.Binary v) => B.Binary (KVarSubst b v)
+instance (B.Binary b, B.Binary v) => B.Binary (ExprBV b v)
 instance B.Binary v => B.Binary (ReftV v)
 
 
@@ -195,7 +211,7 @@
 concConjuncts e = filter isConc (conjuncts e)
 
 isKvar :: Expr -> Bool
-isKvar (PKVar _ _) = True
+isKvar (PKVar {}) = True
 isKvar _           = False
 
 --------------------------------------------------------------------------------
@@ -219,35 +235,62 @@
 instance Hashable SymConst
 instance Hashable Constant
 instance Hashable v => Hashable (SubstV v)
-instance Hashable v => Hashable (ExprV v)
+instance (Hashable b, Hashable v) => Hashable (KVarSubst b v)
+instance (Hashable b, Hashable v) => Hashable (ExprBV b v)
 instance Hashable v => Hashable (ReftV v)
 
 --------------------------------------------------------------------------------
 -- | Substitutions -------------------------------------------------------------
 --------------------------------------------------------------------------------
 type Subst = SubstV Symbol
-newtype SubstV v = Su (M.HashMap Symbol (ExprV v))
-                deriving (Eq, Data, Ord, Typeable, Generic, Functor, Foldable, Traversable)
+newtype SubstV v = Su (M.HashMap v (ExprBV v v))
+                deriving (Eq, Data, Ord, Typeable, Generic)
 
 instance ToJSON Subst
 instance FromJSON Subst
 
-instance (Fixpoint v, Ord v, Show v) => Show (SubstV v) where
+instance (Fixpoint v, Ord v, Hashable v, Show v) => Show (SubstV v) where
   show = showFix
 
-instance (Ord v, Fixpoint v) => Fixpoint (SubstV v) where
-  toFix (Su m) = case hashMapToAscList m of
-                   []  -> empty
-                   xys -> hcat $ map (\(x,y) -> brackets $ toFix x <-> text ":=" <-> toFix y) xys
+instance (Ord v, Hashable v, Fixpoint v) => Fixpoint (SubstV v) where
+  toFix (Su m) = toFix m
 
-instance (Ord v, Fixpoint v) => PPrint (SubstV v) where
+instance (Ord v, Hashable v, Fixpoint v) => PPrint (SubstV v) where
   pprintTidy _ = toFix
 
+newtype KVarSubst b v = KSu [(b, ExprBV b v)]
+  deriving (Eq, Ord, Data, Typeable, Generic, Functor, Foldable, Traversable)
+
+fromKVarSubst :: Hashable b => KVarSubst b v -> M.HashMap b (ExprBV b v)
+fromKVarSubst (KSu su) = M.fromList su
+
+toKVarSubst :: M.HashMap b (ExprBV b v) -> KVarSubst b v
+toKVarSubst = KSu . M.toList
+
+mapKVarSubst :: (ExprBV b v -> ExprBV b v) -> KVarSubst b v -> KVarSubst b v
+mapKVarSubst f (KSu su) = KSu $ fmap (fmap f) su
+
+mapBindKVarSubst :: (Hashable b, Hashable b') => (b -> b') -> KVarSubst b v -> KVarSubst b' v
+mapBindKVarSubst f = toKVarSubst . fmap (mapBindExpr f) . M.mapKeys f . fromKVarSubst
+
+isEmptyKVarSubst :: KVarSubst b v -> Bool
+isEmptyKVarSubst (KSu su) = null su
+
+instance (Ord v, Fixpoint v, Ord b, Fixpoint b, Hashable b) => Show (KVarSubst b v) where
+  show = showFix
+
+instance (Ord v, Fixpoint v, Ord b, Fixpoint b, Hashable b) => Fixpoint (KVarSubst b v) where
+  toFix = toFix . fromKVarSubst
+
+instance (Ord v, Fixpoint v, Ord b, Fixpoint b, Hashable b) => PPrint (KVarSubst b v) where
+  pprintTidy _ = toFix
+
 data KVSub = KVS
   { ksuVV    :: Symbol
   , ksuSort  :: Sort
   , ksuKVar  :: KVar
-  , ksuSubst :: Subst
+  , ksuSubst :: KVarSubst Symbol Symbol
+  , ksuTySub :: M.HashMap Symbol Sort  -- ^ Type variable substitution
   } deriving (Eq, Data, Typeable, Generic, Show)
 
 instance PPrint KVSub where
@@ -277,39 +320,46 @@
 instance ToJSON Constant  where
 instance ToJSON Brel      where
 instance ToJSON Bop       where
+instance ToJSON (KVarSubst Symbol Symbol) where
 instance ToJSON Expr      where
 
 instance FromJSON Constant  where
 instance FromJSON Brel      where
 instance FromJSON Bop       where
+instance FromJSON (KVarSubst Symbol Symbol) where
 instance FromJSON Expr      where
 
 
 type Expr = ExprV Symbol
+type ExprV v = ExprBV Symbol v
+type TyVarSubst = M.HashMap Symbol Sort
 
-data ExprV v
+data ExprBV b v
           = ESym !SymConst
           | ECon !Constant
           | EVar !v
-          | EApp !(ExprV v) !(ExprV v)
-          | ENeg !(ExprV v)
-          | EBin !Bop !(ExprV v) !(ExprV v)
-          | ELet !Symbol !(ExprV v) !(ExprV v)
-          | EIte !(ExprV v) !(ExprV v) !(ExprV v)
-          | ECst !(ExprV v) !Sort
-          | ELam !(Symbol, Sort)   !(ExprV v)
-          | ETApp !(ExprV v) !Sort
-          | ETAbs !(ExprV v) !Symbol
-          | PAnd   ![ExprV v]
-          | POr    ![ExprV v]
-          | PNot   !(ExprV v)
-          | PImp   !(ExprV v) !(ExprV v)
-          | PIff   !(ExprV v) !(ExprV v)
-          | PAtom  !Brel  !(ExprV v) !(ExprV v)
-          | PKVar  !KVar !(SubstV v)
-          | PAll   ![(Symbol, Sort)] !(ExprV v)
-          | PExist ![(Symbol, Sort)] !(ExprV v)
-          | ECoerc !Sort !Sort !(ExprV v)
+          | EApp !(ExprBV b v) !(ExprBV b v)
+          | ENeg !(ExprBV b v)
+          | EBin !Bop !(ExprBV b v) !(ExprBV b v)
+          | ELet !b !(ExprBV b v) !(ExprBV b v)
+          | EIte !(ExprBV b v) !(ExprBV b v) !(ExprBV b v)
+          | ECst !(ExprBV b v) !Sort
+          | ELam !(b, Sort)   !(ExprBV b v)
+          | ETApp !(ExprBV b v) !Sort
+          | ETAbs !(ExprBV b v) !b
+          | PAnd   ![ExprBV b v]
+          | POr    ![ExprBV b v]
+          | PNot   !(ExprBV b v)
+          | PImp   !(ExprBV b v) !(ExprBV b v)
+          | PIff   !(ExprBV b v) !(ExprBV b v)
+          | PAtom  !Brel  !(ExprBV b v) !(ExprBV b v)
+            -- | In @PKVar k su tsu@, @k@ is the KVar, @su@ is the substitution
+            -- for that KVar, and @tsu@ indicates how to instantiate type
+            -- variables that could appear in the KVar solution.
+          | PKVar  !KVar !TyVarSubst !(KVarSubst b v)
+          | PAll   ![(b, Sort)] !(ExprBV b v)
+          | PExist ![(b, Sort)] !(ExprBV b v)
+          | ECoerc !Sort !Sort !(ExprBV b v)
           deriving (Eq, Show, Ord, Data, Typeable, Generic, Functor, Foldable, Traversable)
 
 onEverySubexpr :: (Expr -> Expr) -> Expr -> Expr
@@ -325,34 +375,60 @@
 
 type Pred = Expr
 
-pattern PTrue :: ExprV v
+pattern PTrue :: ExprBV b v
 pattern PTrue = PAnd []
 
-pattern PTop :: ExprV v
+pattern PTop :: ExprBV b v
 pattern PTop = PAnd []
 
-pattern PFalse :: ExprV v
+pattern PFalse :: ExprBV b v
 pattern PFalse = POr  []
 
-pattern EBot :: ExprV v
+pattern EBot :: ExprBV b v
 pattern EBot = POr  []
 
-pattern EEq :: ExprV v -> ExprV v -> ExprV v
+pattern EEq :: ExprBV b v -> ExprBV b v -> ExprBV b v
 pattern EEq e1 e2 = PAtom Eq    e1 e2
 
-pattern ETimes :: ExprV v -> ExprV v -> ExprV v
+pattern ETimes :: ExprBV b v -> ExprBV b v -> ExprBV b v
 pattern ETimes e1 e2 = EBin Times  e1 e2
 
-pattern ERTimes :: ExprV v -> ExprV v -> ExprV v
+pattern ERTimes :: ExprBV b v -> ExprBV b v -> ExprBV b v
 pattern ERTimes e1 e2 = EBin RTimes e1 e2
 
-pattern EDiv :: ExprV v -> ExprV v -> ExprV v
+pattern EDiv :: ExprBV b v -> ExprBV b v -> ExprBV b v
 pattern EDiv e1 e2 = EBin Div    e1 e2
 
-pattern ERDiv :: ExprV v -> ExprV v -> ExprV v
+pattern ERDiv :: ExprBV b v -> ExprBV b v -> ExprBV b v
 pattern ERDiv e1 e2 = EBin RDiv   e1 e2
 
-exprSymbolsSet :: Expr -> HashSet Symbol
+mapBindExpr :: (Hashable b, Hashable b') => (b -> b') -> ExprBV b v -> ExprBV b' v
+mapBindExpr f = go
+  where
+    go (ESym c) = ESym c
+    go (ECon c) = ECon c
+    go (EVar v) = EVar v
+    go (EApp e1 e2) = EApp (go e1) (go e2)
+    go (ENeg e) = ENeg (go e)
+    go (EBin op e1 e2) = EBin op (go e1) (go e2)
+    go (ELet b e1 e2) = ELet (f b) (go e1) (go e2)
+    go (EIte e1 e2 e3) = EIte (go e1) (go e2) (go e3)
+    go (ECst e s) = ECst (go e) s
+    go (ELam (b, s) e) = ELam (f b, s) (go e)
+    go (ETApp e s) = ETApp (go e) s
+    go (ETAbs e b) = ETAbs (go e) (f b)
+    go (PAnd es) = PAnd (go <$> es)
+    go (POr es) = POr (go <$> es)
+    go (PNot e) = PNot (go e)
+    go (PImp e1 e2) = PImp (go e1) (go e2)
+    go (PIff e1 e2) = PIff (go e1) (go e2)
+    go (PAtom rel e1 e2) = PAtom rel (go e1) (go e2)
+    go (PKVar k tsu su) = PKVar k tsu (mapBindKVarSubst f su)
+    go (PAll bs e) = PAll (first f <$> bs) (go e)
+    go (PExist bs e) = PExist (first f <$> bs) (go e)
+    go (ECoerc s1 s2 e) = ECoerc s1 s2 (go e)
+
+exprSymbolsSet :: (Eq v, Hashable v) => ExprBV v v -> HashSet v
 exprSymbolsSet = go
   where
     gos es                = HashSet.unions (go <$> es)
@@ -371,7 +447,7 @@
     go (PIff p1 p2)       = gos [p1, p2]
     go (PImp p1 p2)       = gos [p1, p2]
     go (PAtom _ e1 e2)    = gos [e1, e2]
-    go (PKVar _ (Su su))  = HashSet.unions $ map exprSymbolsSet (M.elems su)
+    go (PKVar _ _ su)       = HashSet.unions $ map exprSymbolsSet (M.elems $ fromKVarSubst su)
     go (PAll xts p)       = go p `HashSet.difference` HashSet.fromList (fst <$> xts)
     go (PExist xts p)     = go p `HashSet.difference` HashSet.fromList (fst <$> xts)
     go _                  = HashSet.empty
@@ -399,7 +475,7 @@
       ECoerc t0 t1 e -> ECoerc (sortSubst f t0) (sortSubst f t1) e
       e -> e
 
-exprKVars :: Expr -> HashMap KVar [Subst]
+exprKVars :: Expr -> HashMap KVar [KVarSubst Symbol Symbol]
 exprKVars = go
   where
     gos es                = HashMap.unions (go <$> es)
@@ -418,19 +494,19 @@
     go (PIff p1 p2)       = gos [p1, p2]
     go (PImp p1 p2)       = gos [p1, p2]
     go (PAtom _ e1 e2)    = gos [e1, e2]
-    go (PKVar k substs@(Su su))  =
-      HashMap.insertWith (++) k [substs] $ HashMap.unions $ map exprKVars (M.elems su)
+    go (PKVar k _ su) =
+      HashMap.insertWith (++) k [su] $ HashMap.unions $ map exprKVars (M.elems $ fromKVarSubst su)
     go (PAll _xts p)       = go p
     go (PExist _xts p)     = go p
     go _                  = HashMap.empty
 
-mkEApp :: LocSymbol -> [Expr] -> Expr
+mkEApp :: Located v -> [ExprBV b v] -> ExprBV b v
 mkEApp = eApps . EVar . val
 
-eApps :: ExprV v -> [ExprV v] -> ExprV v
+eApps :: ExprBV b v -> [ExprBV b v] -> ExprBV b v
 eApps f es  = foldl' EApp f es
 
-splitEApp :: ExprV v -> (ExprV v, [ExprV v])
+splitEApp :: ExprBV b v -> (ExprBV b v, [ExprBV b v])
 splitEApp = go []
   where
     go acc (EApp f e) = go (e:acc) f
@@ -482,16 +558,20 @@
     go (PAtom _ e1 e2) = go e1 + go e2
     go (PAll _ e)      = go e
     go (PExist _ e)    = go e
-    go (PKVar _ _)     = 1
+    go (PKVar {})        = 1
     go (ECoerc _ _ e)  = go e
 
 type Reft = ReftV Symbol
+type ReftV v = ReftBV Symbol v
 
 -- | Refinement of @v@ satisfying a predicate
 --   e.g. in '{x: _ | e }' x is the @Symbol@ and e the @ExprV v@
-newtype ReftV v = Reft (Symbol, ExprV v)
+newtype ReftBV b v = Reft (b, ExprBV b v)
     deriving (Eq, Ord, Data, Typeable, Generic, Functor, Foldable, Traversable)
 
+mapBindReft :: (Hashable b, Hashable b') => (b -> b') -> ReftBV b v -> ReftBV b' v
+mapBindReft f (Reft (b, e)) = Reft (f b, mapBindExpr f e)
+
 data SortedReft = RR { sr_sort :: !Sort, sr_reft :: !Reft }
                   deriving (Eq, Ord, Data, Typeable, Generic)
 
@@ -549,7 +629,7 @@
   toFix RDiv   = text "/."
   toFix Mod    = text "mod"
 
-instance (Ord v, Fixpoint v) => Fixpoint (ExprV v) where
+instance (Ord b, Fixpoint b, Hashable b, Ord v, Fixpoint v) => Fixpoint (ExprBV b v) where
   toFix (ESym c)       = toFix c
   toFix (ECon c)       = toFix c
   toFix (EVar s)       = toFix s
@@ -570,7 +650,7 @@
   toFix (PAnd ps)      = text "&&" <+> toFix ps
   toFix (POr  ps)      = text "||" <+> toFix ps
   toFix (PAtom r e1 e2)  = parens $ sep [ toFix e1 <+> toFix r, nest 2 (toFix e2)]
-  toFix (PKVar k su)     = toFix k <-> toFix su
+  toFix (PKVar k tsu su)   = toFix k <-> toFixTySub tsu <-> toFix su
   toFix (PAll xts p)     = parens $ "forall" <+> (toFix xts
                                         $+$ ("." <+> toFix p))
   toFix (PExist xts p)   = parens $ "exists" <+> (toFix xts
@@ -580,11 +660,23 @@
   toFix (ECoerc a t e)   = parens (text "coerce" <+> toFix a <+> text "~" <+> toFix t <+> text "in" <+> toFix e)
   toFix (ELam (x,s) e)   = parens (char '\\' <+> toFix x <+> ":" <+> toFix s <+> "->" <+> toFix e)
 
-  simplify = simplifyExpr dedup
-    where
-      dedup = Set.toList . Set.fromList
+  simplify = simplifyExprDefault
 
-simplifyExpr :: Eq v => ([ExprV v] -> [ExprV v]) -> ExprV v -> ExprV v
+-- | Serialize a type-variable substitution for PKVar in .fq files.
+-- An empty substitution is rendered as @[@]@, and a non-empty one as
+-- @[\@sym:=sort;...]@.
+toFixTySub :: M.HashMap Symbol Sort -> Doc
+toFixTySub tsu
+  | M.null tsu = empty
+  | otherwise  = brackets (text "@" <->  tyPairs)
+  where
+    tyPairs = hcat $ punctuate (text ";") (toFixTyPair <$> hashMapToAscList tsu)
+    toFixTyPair (s, srt) = toFix s <-> text ":=" <-> toFix srt
+
+simplifyExprDefault :: (Ord b, Ord v) => ExprBV b v -> ExprBV b v
+simplifyExprDefault = simplifyExpr (Set.toList . Set.fromList)
+
+simplifyExpr :: (Eq b, Eq v) => ([ExprBV b v] -> [ExprBV b v]) -> ExprBV b v -> ExprBV b v
 simplifyExpr dedup = go
   where
     go (POr  [])     = PFalse
@@ -629,7 +721,7 @@
       | isTautoPred  p     = PTrue
       | otherwise          = p
 
-isContraPred   :: Eq v => ExprV v -> Bool
+isContraPred   :: (Eq b, Eq v) => ExprBV b v -> Bool
 isContraPred z = eqC z || (z `elem` contras)
   where
     contras    = [PFalse]
@@ -644,7 +736,7 @@
                = x == y
     eqC _      = False
 
-isTautoPred   :: Eq v => ExprV v -> Bool
+isTautoPred   :: (Eq b, Eq v) => ExprBV b v -> Bool
 isTautoPred z  = z == PTop || z == PTrue || eqT z
   where
     eqT (PAnd [])
@@ -716,7 +808,7 @@
 opPrec Div    = 7
 opPrec RDiv   = 7
 
-instance (Ord v, Fixpoint v, PPrint v) => PPrint (ExprV v) where
+instance (Ord b, Fixpoint b, Hashable b, PPrint b, Ord v, Fixpoint v, PPrint v) => PPrint (ExprBV b v) where
   pprintPrec _ k (ESym c)        = pprintTidy k c
   pprintPrec _ k (ECon c)        = pprintTidy k c
   pprintPrec _ k (EVar s)        = pprintTidy k s
@@ -780,8 +872,8 @@
   pprintPrec _ _ (ETAbs e s)     = "ETAbs" <+> toFix e <+> toFix s
 
 pprintQuant
-  :: (Ord v, Fixpoint v, PPrint v)
-  => Tidy -> Doc -> [(Symbol, Sort)] -> ExprV v -> Doc
+  :: (Ord b, Fixpoint b, Hashable b, PPrint b, Ord v, Fixpoint v, PPrint v)
+  => Tidy -> Doc -> [(b, Sort)] -> ExprBV b v -> Doc
 pprintQuant k d xts p = (d <+> pprintTidy k xts)
                         $+$
                         ("  ." <+> pprintTidy k p)
@@ -884,13 +976,13 @@
 --   so they SHOULD NOT be used inside the solver loop. Instead, use 'conj' which ensures
 --   some basic things but is faster.
 
-pAnd, pOr     :: (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
-pAnd          = simplify . PAnd
+pAnd, pOr     :: (Ord b, Hashable b, Ord v) => ListNE (ExprBV b v) -> ExprBV b v
+pAnd          = simplifyExprDefault . PAnd
 
 pAndNoDedup :: ListNE Pred -> Pred
 pAndNoDedup = simplifyExpr id . PAnd
 
-pOr           = simplify . POr
+pOr           = simplifyExprDefault . POr
 
 infixl 9 &.&
 (&.&) :: Pred -> Pred -> Pred
@@ -900,10 +992,10 @@
 (|.|) :: Pred -> Pred -> Pred
 (|.|) p q = pOr [p, q]
 
-pIte :: (Fixpoint v, Ord v) => ExprV v -> ExprV v -> ExprV v -> ExprV v
+pIte :: (Fixpoint b, Ord b, Hashable b, Fixpoint v, Ord v) => ExprBV b v -> ExprBV b v -> ExprBV b v -> ExprBV b v
 pIte p1 p2 p3 = pAnd [p1 `PImp` p2, PNot p1 `PImp` p3]
 
-pExist :: [(Symbol, Sort)] -> ExprV v -> ExprV v
+pExist :: [(b, Sort)] -> ExprBV b v -> ExprBV b v
 pExist []  p = p
 pExist xts p = PExist xts p
 
@@ -947,13 +1039,13 @@
 isNonTrivial :: SortedReft -> Bool
 isNonTrivial = not . isTautoReft . sr_reft
 
-isTautoReft :: Eq v => ReftV v -> Bool
+isTautoReft :: (Eq b, Eq v) => ReftBV b v -> Bool
 isTautoReft = all isTautoPred . conjuncts . reftPred
 
-reftPred :: ReftV v -> ExprV v
+reftPred :: ReftBV b v -> ExprBV b v
 reftPred (Reft (_, p)) = p
 
-reftBind :: ReftV v -> Symbol
+reftBind :: ReftBV b v -> b
 reftBind (Reft (x, _)) = x
 
 ------------------------------------------------------------
@@ -972,18 +1064,18 @@
 trueSortedReft :: Sort -> SortedReft
 trueSortedReft = (`RR` trueReft)
 
-trueReft, falseReft :: ReftV v
-trueReft  = Reft (vv_, PTrue)
-falseReft = Reft (vv_, PFalse)
+trueReft, falseReft :: Binder b => ReftBV b v
+trueReft  = Reft (wildcard, PTrue)
+falseReft = Reft (wildcard, PFalse)
 
-flattenRefas :: [ExprV v] -> [ExprV v]
+flattenRefas :: [ExprBV b v] -> [ExprBV b v]
 flattenRefas        = flatP []
   where
     flatP acc (PAnd ps:xs) = flatP (flatP acc xs) ps
     flatP acc (p:xs)       = p : flatP acc xs
     flatP acc []           = acc
 
-conjuncts :: Eq v => ExprV v -> [ExprV v]
+conjuncts :: (Eq b, Eq v) => ExprBV b v -> [ExprBV b v]
 conjuncts (PAnd ps) = concatMap conjuncts ps
 conjuncts p
   | isTautoPred p   = []
@@ -997,28 +1089,32 @@
 class Falseable a where
   isFalse :: a -> Bool
 
-instance Falseable Expr where
+instance Falseable (ExprBV b v) where
   isFalse PFalse = True
   isFalse _      = False
 
-instance Falseable Reft where
+instance Falseable (ReftBV b v) where
   isFalse (Reft (_, ra)) = isFalse ra
 
 -------------------------------------------------------------------------
 -- | Class Predicates for Valid Refinements -----------------------------
 -------------------------------------------------------------------------
 
-class Subable a where
-  syms   :: a -> [Symbol]                   -- ^ free symbols of a
-  substa :: (Symbol -> Symbol) -> a -> a
+class (Eq (Variable a), Hashable (Variable a)) => Subable a where
+  type Variable a
+  type Variable a = Symbol
+
+  syms   :: a -> [Variable a]                   -- ^ free symbols of a
+  substa :: (Variable a -> Variable a) -> a -> a
   -- substa f  = substf (EVar . f)
 
-  substf :: (Symbol -> Expr) -> a -> a
-  subst  :: HasCallStack => Subst -> a -> a
-  subst1 :: a -> (Symbol, Expr) -> a
+  substf :: (Variable a -> ExprBV (Variable a) (Variable a)) -> a -> a
+  subst  :: HasCallStack => SubstV (Variable a) -> a -> a
+  subst1 :: a -> (Variable a, ExprBV (Variable a) (Variable a)) -> a
   subst1 y (x, e) = subst (Su $ M.fromList [(x,e)]) y
 
 instance Subable a => Subable (Located a) where
+  type Variable (Located a) = Variable a
   syms (Loc _ _ x)   = syms x
   substa f (Loc l l' x) = Loc l l' (substa f x)
   substf f (Loc l l' x) = Loc l l' (substf f x)
diff --git a/src/Language/Fixpoint/Types/SMTPrint.hs b/src/Language/Fixpoint/Types/SMTPrint.hs
--- a/src/Language/Fixpoint/Types/SMTPrint.hs
+++ b/src/Language/Fixpoint/Types/SMTPrint.hs
@@ -92,7 +92,8 @@
 instance ToHornSMT F.Subst where
   toHornSMT (F.Su m) = toHornSMT (Misc.hashMapToAscList m)
 
-
+instance ToHornSMT (F.KVarSubst F.Symbol F.Symbol) where
+  toHornSMT = toHornSMT . Misc.hashMapToAscList . F.fromKVarSubst
 
 instance ToHornSMT F.KVar where
   toHornSMT (F.KV k) = "$" P.<-> toHornSMT k
@@ -122,7 +123,7 @@
 toHornExpr (F.PExist xts p)  = toHornMany ["exists", toHornSMT xts, toHornSMT p]
 toHornExpr (F.ELam b e)      = toHornMany ["lam", toHornSMT b, toHornSMT e]
 toHornExpr (F.ECoerc a t e)  = toHornMany ["coerce", toHornSMT a, toHornSMT t, toHornSMT e]
-toHornExpr (F.PKVar k su)    = toHornMany [toHornSMT k, toHornSMT su]
+toHornExpr (F.PKVar k _ su)    = toHornMany [toHornSMT k, toHornSMT su]
 toHornExpr (F.ETApp e s)     = toHornMany ["ETApp" , toHornSMT e, toHornSMT s]
 toHornExpr (F.ETAbs e s)     = toHornMany ["ETAbs" , toHornSMT e, toHornSMT s]
 
diff --git a/src/Language/Fixpoint/Types/Solutions.hs b/src/Language/Fixpoint/Types/Solutions.hs
--- a/src/Language/Fixpoint/Types/Solutions.hs
+++ b/src/Language/Fixpoint/Types/Solutions.hs
@@ -47,13 +47,12 @@
 
   -- * Manipulating QBind
   , qb
-  , qbPreds
   , qbFilter
   , qbFilterM
 
 
   -- * Conversion for client
-  , result 
+  , result
 
   -- * "Fast" Solver (DEPRECATED as unsound)
   , Index  (..)
@@ -186,13 +185,7 @@
 --------------------------------------------------------------------------------
 result s = pAnd . fmap eqPred . qbEQuals <$> sMap s
 
-
 --------------------------------------------------------------------------------
-qbPreds :: Subst -> QBind -> [(Pred, EQual)]
---------------------------------------------------------------------------------
-qbPreds su (QB eqs) =  [ (subst su $ eqPred eq, eq) | eq <- eqs ]
-
---------------------------------------------------------------------------------
 -- | Read / Write Solution at KVar ---------------------------------------------
 --------------------------------------------------------------------------------
 lookupQBind :: Sol QBind -> KVar -> QBind
@@ -249,13 +242,16 @@
 
 instance NFData EQual
 
--- | @eQual q xs@ instantiates @q@ with the arguments in @xs@
-eQual :: Qualifier -> [Symbol] -> EQual
-eQual q xs = {- tracepp "eQual" $ -} EQL q p es
+-- | @eQual q xs ls@ instantiates @q@ with variable arguments @xs@ and literal arguments @ls@
+eQual :: Qualifier -> [Symbol] -> [Constant] -> EQual
+eQual q xs ls = {- tracepp "eQual" $ -} EQL q p es
   where
     p      = subst su $  qBody q
-    su     = mkSubst  $  safeZip "eQual" qxs es
-    es     = eVar    <$> xs
+    su     = mkSubst  $  safeZip "eQual" qxs (reverse es)
+    (es, _, _) = L.foldl' go ([], xs, ls) (qParams q)
+    go (acc, x:xs', cs   ) qp | qpPat qp /= PatLit = (eVar x : acc, xs', cs)
+    go (acc, xs',   c:cs') qp | qpPat qp == PatLit = (ECon c : acc, xs', cs')
+    go _                   _                       = error "eQual: mismatched params"
     qxs    = qpSym   <$> qParams q
 
 --------------------------------------------------------------------------------
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
@@ -31,6 +31,7 @@
   , boolFTyCon
   , realFTyCon
   , numFTyCon
+  , fracFTyCon
   , strFTyCon
   , setFTyCon
   , mapFTyCon -- TODO: hide these
@@ -67,6 +68,7 @@
   , mkPoly
   , sortSymbols
   , substSort
+  , matchSortsTyVars
 
   , isBool, isNumeric, isReal, isString, isSet, isMap, isBag, isArray, isFinfield, isPolyInst
 
@@ -153,12 +155,13 @@
 defRealInfo = False
 defStrInfo  = False
 
-charFTyCon, intFTyCon, boolFTyCon, realFTyCon, funcFTyCon, numFTyCon :: FTycon
+charFTyCon, intFTyCon, boolFTyCon, realFTyCon, funcFTyCon, numFTyCon, fracFTyCon :: FTycon
 strFTyCon, listFTyCon, mapFTyCon, bagFTyCon, setFTyCon, ffldFTyCon :: FTycon
 intFTyCon  = TC (dummyLoc "int"       ) numTcInfo
 boolFTyCon = TC (dummyLoc boolLConName) defTcInfo
 realFTyCon = TC (dummyLoc "real"      ) realTcInfo
 numFTyCon  = TC (dummyLoc "num"       ) numTcInfo
+fracFTyCon = TC (dummyLoc "frac"      ) realTcInfo
 funcFTyCon = TC (dummyLoc "function"  ) defTcInfo
 strFTyCon  = TC (dummyLoc strConName  ) strTcInfo
 listFTyCon = TC (dummyLoc listConName ) defTcInfo
@@ -268,6 +271,7 @@
 sortFTycon :: Sort -> Maybe FTycon
 sortFTycon FInt    = Just intFTyCon
 sortFTycon FReal   = Just realFTyCon
+sortFTycon FFrac   = Just fracFTyCon
 sortFTycon FNum    = Just numFTyCon
 sortFTycon (FTC c) = Just c
 sortFTycon _       = Nothing
@@ -341,6 +345,25 @@
   FAbs i t -> FAbs i (substSort f t)
   t -> t
 
+-- | @matchSortsTyVars tvs wfSort useSiteSort@ structurally matches two sorts and
+-- extracts a mapping from type variable symbols (in @tvs@) to their
+-- instantiation at the use site. For example:
+--
+-- > matchSortsTyVars ["a"] (FApp listTC (FObj "a")) (FApp listTC (FObj "b"))
+-- >   == HashMap.fromList [("a", FObj "b")]
+matchSortsTyVars :: [Symbol] -> Sort -> Sort -> M.HashMap Symbol Sort
+matchSortsTyVars tvs wfSort useSiteSort
+  | null tvs  = M.empty
+  | otherwise = go M.empty wfSort useSiteSort
+  where
+    tvSet = HashSet.fromList tvs
+    go acc (FObj s) t
+      | HashSet.member s tvSet = if FObj s /= t then M.insert s t acc else acc
+    go acc (FFunc a1 a2) (FFunc b1 b2) = go (go acc a1 b1) a2 b2
+    go acc (FApp a1 a2) (FApp b1 b2) = go (go acc a1 b1) a2 b2
+    go acc (FAbs _ a) (FAbs _ b) = go acc a b
+    go acc _ _ = acc
+
 data DataField = DField
   { dfName :: !LocSymbol          -- ^ Field Name
   , dfSort :: !Sort               -- ^ Field Sort
@@ -600,6 +623,7 @@
 fTyconSort c
   | c == intFTyCon  = FInt
   | c == realFTyCon = FReal
+  | c == fracFTyCon = FFrac
   | c == numFTyCon  = FNum
   | otherwise       = FTC c
 
diff --git a/src/Language/Fixpoint/Types/Spans.hs b/src/Language/Fixpoint/Types/Spans.hs
--- a/src/Language/Fixpoint/Types/Spans.hs
+++ b/src/Language/Fixpoint/Types/Spans.hs
@@ -163,11 +163,11 @@
   toFix = text . show
 
 
-data Located a = Loc 
+data Located a = Loc
   { loc  :: !SourcePos -- ^ Start Position
   , locE :: !SourcePos -- ^ End Position
   , val  :: !a
-  } 
+  }
   deriving (Data, Typeable, Generic, ToJSON, FromJSON)
 
 instance ToJSON SourcePos where
@@ -223,7 +223,7 @@
 instance (B.Binary a) => B.Binary (Located a)
 
 
-instance ToJSON Pos where 
+instance ToJSON Pos where
 
 instance FromJSON Pos where
 
diff --git a/src/Language/Fixpoint/Types/Substitutions.hs b/src/Language/Fixpoint/Types/Substitutions.hs
--- a/src/Language/Fixpoint/Types/Substitutions.hs
+++ b/src/Language/Fixpoint/Types/Substitutions.hs
@@ -1,5 +1,7 @@
 {-# LANGUAGE CPP               #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies      #-}
+{-# LANGUAGE TypeOperators     #-}
 
 {-# OPTIONS_GHC -Wno-orphans   #-}
 {-# LANGUAGE InstanceSigs #-}
@@ -9,11 +11,16 @@
 --   be in the same place as the @Term@ definitions.
 module Language.Fixpoint.Types.Substitutions (
     mkSubst
+  , mkKVarSubst
+  , substFromKSubst
+  , kSubstFromSubst
+  , ksubst
   , isEmptySubst
   , substExcept
   , substfExcept
   , subst1Except
   , substSymbolsSet
+  , Refreshable(..)
   , rapierSubstExpr
   , targetSubstSyms
   , filterSubst
@@ -26,8 +33,10 @@
 
 import           Data.List                 as List
 import           Data.Maybe
+import           Data.Hashable             (Hashable)
 import qualified Data.HashMap.Strict       as M
 import qualified Data.HashSet              as S
+import           Language.Fixpoint.Types.Binders
 import           Language.Fixpoint.Types.PrettyPrint
 import           Language.Fixpoint.Types.Names
 import           Language.Fixpoint.Types.Sorts
@@ -36,37 +45,56 @@
 import           Text.PrettyPrint.HughesPJ.Compat
 import           Text.Printf               (printf)
 
-instance Semigroup Subst where
+instance (Eq v, Hashable v) => Semigroup (SubstV v) where
   (<>) = catSubst
 
-instance Monoid Subst where
+instance (Eq v, Hashable v) => Monoid (SubstV v) where
   mempty  = emptySubst
   mappend = (<>)
 
-filterSubst :: (Symbol -> Expr -> Bool) -> Subst -> Subst
+instance Semigroup (KVarSubst Symbol Symbol) where
+  su1 <> su2 = kSubstFromSubst $ substFromKSubst su1 <> substFromKSubst su2
+
+instance Monoid (KVarSubst Symbol Symbol) where
+  mempty = kSubstFromSubst mempty
+  mappend = (<>)
+
+substFromKSubst :: Hashable v => KVarSubst v v -> SubstV v
+substFromKSubst = Su . fromKVarSubst
+
+kSubstFromSubst :: SubstV v -> KVarSubst v v
+kSubstFromSubst (Su m) = toKVarSubst m
+
+ksubst :: KVarSubst Symbol Symbol -> Expr -> Expr
+ksubst = subst . substFromKSubst
+
+filterSubst :: (v -> ExprBV v v -> Bool) -> SubstV v -> SubstV v
 filterSubst f (Su m) = Su (M.filterWithKey f m)
 
-emptySubst :: Subst
+emptySubst :: SubstV v
 emptySubst = Su M.empty
 
-catSubst :: Subst -> Subst -> Subst
+catSubst :: (Eq v, Hashable v) => SubstV v -> SubstV v -> SubstV v
 catSubst (Su s1) θ2@(Su s2) = Su $ M.union s1' s2
   where
     s1'                     = subst θ2 <$> s1
 
-mkSubst :: [(Symbol, Expr)] -> Subst
+mkSubst :: Hashable v => [(v, ExprBV v v)] -> SubstV v
 mkSubst = Su . M.fromList . reverse . filter notTrivial
   where
     notTrivial (x, EVar y) = x /= y
     notTrivial _           = True
 
-isEmptySubst :: Subst -> Bool
+mkKVarSubst :: [(Symbol, Expr)] -> KVarSubst Symbol Symbol
+mkKVarSubst = kSubstFromSubst . mkSubst
+
+isEmptySubst :: SubstV v -> Bool
 isEmptySubst (Su xes) = M.null xes
 
-targetSubstSyms :: Subst -> [Symbol]
+targetSubstSyms :: (Eq v, Hashable v) => SubstV v -> [v]
 targetSubstSyms (Su ms) = syms $ M.elems ms
 
-substSymbolsSet :: Subst -> S.HashSet Symbol
+substSymbolsSet :: (Eq v, Hashable v) => SubstV v -> S.HashSet v
 substSymbolsSet (Su m) = S.unions $ map exprSymbolsSet (M.elems m)
 
 instance Subable () where
@@ -75,19 +103,22 @@
   substf _ () = ()
   substa _ () = ()
 
-instance (Subable a, Subable b) => Subable (a,b) where
+instance (Subable a, Subable b, Variable a ~ Variable b) => Subable (a,b) where
+  type Variable (a, b) = Variable a
   syms  (x, y)   = syms x ++ syms y
   subst su (x,y) = (subst su x, subst su y)
   substf f (x,y) = (substf f x, substf f y)
   substa f (x,y) = (substa f x, substa f y)
 
 instance Subable a => Subable [a] where
+  type Variable [a] = Variable a
   syms   = concatMap syms
   subst  = fmap . subst
   substf = fmap . substf
   substa = fmap . substa
 
 instance Subable a => Subable (Maybe a) where
+  type Variable (Maybe a) = Variable a
   syms   = concatMap syms . maybeToList
   subst  = fmap . subst
   substf = fmap . substf
@@ -95,20 +126,21 @@
 
 
 instance Subable a => Subable (M.HashMap k a) where
+  type Variable (M.HashMap k a) = Variable a
   syms   = syms . M.elems
   subst  = M.map . subst
   substf = M.map . substf
   substa = M.map . substa
 
-subst1Except :: (Subable a) => [Symbol] -> a -> (Symbol, Expr) -> a
+subst1Except :: Subable a => [Variable a] -> a -> (Variable a, ExprBV (Variable a) (Variable a)) -> a
 subst1Except xs z su@(x, _)
   | x `elem` xs = z
   | otherwise   = subst1 z su
 
-substfExcept :: (Symbol -> Expr) -> [Symbol] -> Symbol -> Expr
+substfExcept :: Eq v => (v -> ExprBV b v) -> [v] -> v -> ExprBV b v
 substfExcept f xs y = if y `elem` xs then EVar y else f y
 
-substExcept  :: Subst -> [Symbol] -> Subst
+substExcept  :: Eq v => SubstV v -> [v] -> SubstV v
 -- substExcept  (Su m) xs = Su (foldr M.delete m xs)
 substExcept (Su xes) xs = Su $ M.filterWithKey (const . not . (`elem` xs)) xes
 
@@ -118,21 +150,22 @@
   subst su x               = subSymbol (Just $ appSubst su x) x -- subSymbol (M.lookup x s) x
   syms x                   = [x]
 
-appSubst :: Subst -> Symbol -> Expr
+appSubst :: (Eq v, Hashable v) => SubstV v -> v -> ExprBV v v
 appSubst (Su s) x = fromMaybe (EVar x) (M.lookup x s)
 
-subSymbol :: Maybe Expr -> Symbol -> Symbol
+subSymbol :: (Ord v, Hashable v, Fixpoint v) => Maybe (ExprBV v v) -> v -> v
 subSymbol (Just (EVar y)) _ = y
 subSymbol Nothing         x = x
 subSymbol a               b = errorstar (printf "Cannot substitute symbol %s with expression %s" (showFix b) (showFix a))
 
-captureAvoiding :: Symbol -> (Symbol -> Expr) -> Symbol -> Expr
+captureAvoiding :: Eq v => v -> (v -> ExprBV b v) -> v -> ExprBV b v
 captureAvoiding x f y = if y == x then EVar x else f y
 
-instance Subable Expr where
+instance (Eq v, Hashable v) => Subable (ExprBV v v) where
+  type Variable (ExprBV v v) = v
   syms                     = exprSymbols
   substa f                 = substf (EVar . f)
-  substf :: (Symbol -> Expr) -> Expr -> Expr
+  substf :: (v -> ExprBV v v) -> ExprBV v v -> ExprBV v v
   substf f (EApp s e)      = EApp (substf f s) (substf f e)
   substf f (ELam (x,t) e)  = ELam (x, t) (substf (captureAvoiding x f) e)
   substf f (ECoerc a t e)  = ECoerc a t (substf f e)
@@ -148,7 +181,7 @@
   substf f (PImp p1 p2)    = PImp (substf f p1) (substf f p2)
   substf f (PIff p1 p2)    = PIff (substf f p1) (substf f p2)
   substf f (PAtom r e1 e2) = PAtom r (substf f e1) (substf f e2)
-  substf f (PKVar k (Su su)) = PKVar k (Su $ M.map (substf f) su)
+  substf f (PKVar k tsu su)    = PKVar k tsu (mapKVarSubst (substf f) su)
   substf _ (PAll _ _)      = errorstar "substf: FORALL"
   substf f (PExist xts e)  = PExist xts (substf f e)
   substf _  p              = p
@@ -192,39 +225,45 @@
           PIff (go su p1) (go su p2)
         PAtom r e1 e2 ->
           PAtom r (go su e1) (go su e2)
-        PKVar k su' ->
-          PKVar k $ su' `catSubst` su
+        PKVar k tsu su' ->
+          PKVar k tsu (kSubstFromSubst $ substFromKSubst su' `catSubst` su)
         PAll bs p
-          | disjoint su bs ->
-            PAll bs $ go su p --(substExcept su (fst <$> bs)) p
+          | disjointRange su' bs ->
+            PAll bs $ go su' p
           | otherwise ->
-            errorstar $ unlines
-              [ "subst: FORALL without disjoint binds"
-              , "su: " ++ showpp su
-              , "expr: " ++ showpp e0
-              ]
+            errorstar "subst: PAll (without disjoint binds)"
+          where
+            su' = substExcept su (map fst bs)
+
         PExist bs p
-          | disjoint su bs ->
-            PExist bs $ go su p --(substExcept su (fst <$> bs)) p
+          | disjointRange su' bs ->
+            PExist bs $ go su' p
           | otherwise ->
-            errorstar $ unlines
-              [ "subst: EXISTS without disjoint binds"
-              , "su: " ++ showpp su
-              , "expr: " ++ showpp e0
-              ]
+            errorstar "subst: EXISTS without disjoint binds"
+          where
+            su' = substExcept su (map fst bs)
         p ->
           p
 
-removeSubst :: Subst -> Symbol -> Subst
+removeSubst :: (Eq v, Hashable v) => SubstV v -> v -> SubstV v
 removeSubst (Su su) x = Su $ M.delete x su
 
+-- | Variable names for which we can propose variations to avoid name captures
+class Refreshable v where
+  -- | Variations of a variable name. They must contain at least a fresh name in
+  -- the contexts where @candidates@ is used.
+  candidates :: v -> [v]
+
+instance Refreshable Symbol where
+  candidates x = [ renameSubstSymbol x i | i <- [0..] ]
+
 -- | Rapier style capture-avoiding substitution
 --
 -- The scope set parameter must contain any symbols that are expected
 -- to appear free in the result expression. Typically, this is the set of
 -- symbols that are free in the range of the substitution, plus any symbols
 -- that are already free in the input expression.
-rapierSubstExpr :: S.HashSet Symbol -> Subst -> Expr -> Expr
+rapierSubstExpr :: (Hashable v, Refreshable v) => S.HashSet v -> SubstV v -> ExprBV v v -> ExprBV v v
 rapierSubstExpr s su e0 =
   let go = rapierSubstExpr
    in case e0 of
@@ -257,7 +296,7 @@
     PImp p1 p2 -> PImp (go s su p1) (go s su p2)
     PIff p1 p2 -> PIff (go s su p1) (go s su p2)
     PAtom r e1 e2 -> PAtom r (go s su e1) (go s su e2)
-    PKVar k su' -> PKVar k $ catSubstGo su' su
+    PKVar k tsu su' -> PKVar k tsu (catSubstGo su' su)
     PAll bs p ->
       let mfs = map (maybeFresh . fst) bs
           fs = map (either (\x -> (x, x)) id) mfs
@@ -276,38 +315,38 @@
           PExist bs' $ go s' su' p
     p -> p
   where
-    fresh :: Symbol -> Symbol
-    fresh x = head $ dropWhile (`S.member` s) candidates
-      where
-        candidates = [ renameSubstSymbol x i | i <- [0..] ]
+    fresh x = head $ dropWhile (`S.member` s) (candidates x)
 
     maybeFresh x =
       if x `S.member` s then Right (x, fresh x) else Left x
 
-    catSubstGo :: Subst -> Subst -> Subst
-    catSubstGo (Su s1) su2@(Su s2) = Su $ M.union s1' s2
+    catSubstGo su1 su2@(Su s2) = toKVarSubst $ M.union s1 s2
       where
-        s1' = rapierSubstExpr s su2 <$> s1
+        s1 = rapierSubstExpr s su2 <$> fromKVarSubst su1
 
-extendSubst :: Subst -> Symbol -> Expr -> Subst
+extendSubst :: Hashable v => SubstV v -> v -> ExprBV v v -> SubstV v
 extendSubst (Su m) x e = Su $ M.insert x e m
 
-disjoint :: Subst -> [(Symbol, Sort)] -> Bool
-disjoint (Su su) bs = S.null $ suSyms `S.intersection` bsSyms
+disjointRange :: (Eq v, Hashable v) => SubstV v -> [(v, Sort)] -> Bool
+disjointRange (Su su) bs = S.null $ suSyms `S.intersection` bsSyms
   where
-    suSyms = S.fromList $ syms (M.elems su) ++ M.keys su
+    suSyms = S.fromList $ syms (M.elems su)
     bsSyms = S.fromList $ fst <$> bs
 
-meetReft :: Reft -> Reft -> Reft
+meetReft :: Binder v => ReftBV v v -> ReftBV v v -> ReftBV v v
 meetReft (Reft (v, ra)) (Reft (v', ra'))
   | v == v'          = Reft (v , pAnd [ra, ra'])
-  | v == dummySymbol = Reft (v', pAnd [ra', ra `subst1`  (v , EVar v')])
+  | v == wildcard    = Reft (v', pAnd [ra', ra `subst1`  (v , EVar v')])
   | otherwise        = Reft (v , pAnd [ra, ra' `subst1` (v', EVar v )])
 
-instance Subable Reft where
+instance (Eq v, Hashable v, Refreshable v) => Subable (ReftBV v v) where
+  type Variable (ReftBV v v) = v
   syms (Reft (v, ras))      = v : syms ras
   substa f (Reft (v, ras))  = Reft (f v, substa f ras)
-  subst su (Reft (v, ras))  = Reft (v, subst (substExcept su [v]) ras)
+  subst su (Reft (v, ras))  =
+    let su' = substExcept su [v]
+        s = S.union (substSymbolsSet su') (exprSymbolsSet ras)
+     in Reft (v, rapierSubstExpr s su' ras)
   substf f (Reft (v, ras))  = Reft (v, substf (substfExcept f [v]) ras)
   subst1 (Reft (v, ras)) su = Reft (v, subst1Except [v] ras su)
 
@@ -385,7 +424,7 @@
     -- go _                  = []
 
 
-exprSymbols :: Expr -> [Symbol]
+exprSymbols :: (Eq v, Hashable v) => ExprBV v v -> [v]
 exprSymbols = S.toList . exprSymbolsSet
 
 instance Expression (Symbol, SortedReft) where
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
@@ -38,6 +38,7 @@
     , insertSymEnv
     , deleteSymEnv
     , insertsSymEnv
+    , deletesSymEnv
     , symbolAtName
     , symbolAtSortIndex
 
@@ -133,6 +134,7 @@
     -- 'seAppls' stack, and @seApplsCur@ is cleared.
   , seApplsCur :: !(M.HashMap FuncSort Int)
   , seIx       :: !Int                      -- ^ Largest unused index for sorts
+  , seString   :: !Bool                     -- ^ Use string literals
   }
   deriving (Eq, Show, Data, Typeable, Generic)
 
@@ -157,17 +159,19 @@
                     , seAppls    = zipWith (<>) (seAppls e1) (seAppls e2)
                     , seApplsCur = seApplsCur e1 <> seApplsCur e2
                     , seIx       = seIx       e1 `max` seIx    e2
+                    , seString   = seString e1 && seString e2
                     }
 
 instance Monoid SymEnv where
-  mempty        = SymEnv emptySEnv emptySEnv emptySEnv emptySEnv [] mempty 0
+  mempty        = SymEnv emptySEnv emptySEnv emptySEnv emptySEnv [] mempty 0 True
   mappend       = (<>)
 
-symEnv :: SEnv Sort -> SEnv TheorySymbol -> [DataDecl] -> SEnv Sort -> [Sort] -> SymEnv
-symEnv xEnv fEnv ds ls _ = SymEnv xEnv' fEnv dEnv ls [] mempty 0
+symEnv :: Config -> SEnv Sort -> SEnv TheorySymbol -> [DataDecl] -> SEnv Sort -> [Sort] -> SymEnv
+symEnv cfg xEnv fEnv ds ls _ = SymEnv xEnv' fEnv dEnv ls [] mempty 0 seStr
   where
     xEnv'   = unionSEnv xEnv wiredInEnv
     dEnv    = fromListSEnv [(symbol d, d) | d <- ds]
+    seStr   = not (noStringTheory cfg)
 
 -- | These are "BUILT-in" polymorphic functions which are
 --   UNINTERPRETED but POLYMORPHIC, hence need to go through
@@ -193,6 +197,9 @@
 insertsSymEnv :: SymEnv -> [(Symbol, Sort)] -> SymEnv
 insertsSymEnv = L.foldl' (\env (x, s) -> insertSymEnv x s env)
 
+deletesSymEnv :: SymEnv -> [Symbol] -> SymEnv
+deletesSymEnv = L.foldl' (\env x -> deleteSymEnv x env)
+
 symbolAtSortIndex :: Symbol -> Int -> Text
 symbolAtSortIndex mkSym si = appendSymbolText mkSym . Text.pack . show $ si
 
@@ -308,9 +315,13 @@
 --   'smtSort True  msg t' serializes a sort 't' using type variables,
 --   'smtSort False msg t' serializes a sort 't' using 'Int' instead of tyvars.
 sortSmtSort :: Bool -> SEnv DataDecl -> Sort -> SmtSort
-sortSmtSort poly env t = {- tracepp ("sortSmtSort: " ++ showpp t) $ -} go . unAbs $ t
+sortSmtSort poly env t = sortSmtSort' poly env m t
   where
     m = sortAbs t
+
+sortSmtSort' :: Bool -> SEnv DataDecl -> Int -> Sort -> SmtSort
+sortSmtSort' poly env m t = go . unAbs $ t
+  where
     go (FFunc _ _)    = SInt
     go FInt           = SInt
     go FReal          = SReal
@@ -327,16 +338,16 @@
 fappSmtSort :: Bool -> Int -> SEnv DataDecl -> Sort -> [Sort] -> SmtSort
 fappSmtSort poly m env = go
   where
--- HKT    go t@(FVar _) ts            = SApp (sortSmtSort poly env <$> (t:ts))
-
+    -- See https://github.com/ucsd-progsys/liquid-fixpoint/pull/839 for why
+    -- @FAbs m@ is re-added.
     go (FTC c) [a]
-      | setConName == symbol c   = SSet (sortSmtSort poly env a)
+      | setConName == symbol c   = SSet (sortSmtSort' poly env m a)
     go (FTC c) [a]
-      | bagConName == symbol c   = SBag (sortSmtSort poly env a)
+      | bagConName == symbol c   = SBag (sortSmtSort' poly env m a)
     go (FTC c) [FNatNum n]
       | ffldConName == symbol c  = SFFld n
     go (FTC c) [a, b]
-      | arrayConName == symbol c = SArray (sortSmtSort poly env a) (sortSmtSort poly env b)
+      | arrayConName == symbol c = SArray (sortSmtSort' poly env m a) (sortSmtSort' poly env m b)
     go (FTC bv) [FTC s]
       | bitVecName == symbol bv
       , Just n <- sizeBv s      = SBitVec n
@@ -344,7 +355,7 @@
       | isString s              = SString
     go (FTC c) ts
       | Just n <- tyArgs c env
-      , let i = n - length ts   = SData c ((sortSmtSort poly env . FAbs m <$> ts) ++ pad i)
+      , let i = n - length ts   = SData c ((sortSmtSort' poly env m <$> ts) ++ pad i)
     go _ _                      = SInt
 
     pad i | poly                = []
@@ -389,4 +400,5 @@
          , seAppls    = seAppls  env
          , seApplsCur = seApplsCur env
          , seIx       = seIx     env
+         , seString   = seString env
          }
diff --git a/src/Language/Fixpoint/Types/Utils.hs b/src/Language/Fixpoint/Types/Utils.hs
--- a/src/Language/Fixpoint/Types/Utils.hs
+++ b/src/Language/Fixpoint/Types/Utils.hs
@@ -60,7 +60,7 @@
     rs                   = reftConjuncts (sr_reft sr)
     t                    = sr_sort sr
 
-    go ps ks ((v, PKVar k su    ):xs) = go ps (KVS v t k su:ks) xs
+    go ps ks ((v, PKVar k tsu su):xs) = go ps (KVS v t k su tsu:ks) xs
     go ps ks ((_, p):xs)              = go (p:ps) ks xs
     go ps ks []                       = (ps, ks)
 
diff --git a/src/Language/Fixpoint/Types/Visitor.hs b/src/Language/Fixpoint/Types/Visitor.hs
--- a/src/Language/Fixpoint/Types/Visitor.hs
+++ b/src/Language/Fixpoint/Types/Visitor.hs
@@ -16,6 +16,7 @@
 
   -- * Extracting Symbolic Constants (String Literals)
   ,  SymConsts (..)
+  ,  getConstants
 
   -- * Default Visitor
   , defaultFolder
@@ -41,6 +42,7 @@
   , applyCoSub
   , CoSubV
   , applyCoSubV
+  , applyCoercion
 
   -- * Predicates on Constraints
   , isConcC , isConc, isKvarC
@@ -63,6 +65,7 @@
 import GHC.IO (unsafePerformIO)
 import Data.IORef (newIORef, readIORef, IORef, modifyIORef')
 import Prelude hiding (Foldable)
+import Data.Containers.ListUtils (nubOrd)
 
 
 
@@ -127,7 +130,7 @@
       step (PExist xts p)   = PExist xts (vE p)
       step (ETApp e s)      = ETApp (vE e) s
       step (ETAbs e s)      = ETAbs (vE e) s
-      step p@(PKVar _ _)    = p
+      step p@(PKVar {})       = p
 
 instance Visitable Reft where
   transE v (Reft (x, ra)) = Reft (x, transE v ra)
@@ -274,18 +277,19 @@
     step !c (PExist xts p)  = PExist xts  <$> vE c p
     step !c (ETApp e s)     = (`ETApp` s) <$> vE c e
     step !c (ETAbs e s)     = (`ETAbs` s) <$> vE c e
-    step _  p@(PKVar _ _)   = return p
+    step _  p@(PKVar {})    = return p
 
 mapKVars :: Visitable t => (KVar -> Maybe Expr) -> t -> t
 mapKVars f = mapKVars' f'
   where
     f' (kv', _) = f kv'
 
-mapKVars' :: Visitable t => ((KVar, Subst) -> Maybe Expr) -> t -> t
+mapKVars' :: Visitable t => ((KVar, KVarSubst Symbol Symbol) -> Maybe Expr) -> t -> t
 mapKVars' f = trans txK
   where
-    txK (PKVar k su)
-      | Just p' <- f (k, su) = subst su p'
+    txK (PKVar k tsu su)
+      | Just p' <- f (k, su) = ksubst su p'
+      | otherwise = PKVar k tsu su
     txK p = p
 
 
@@ -359,7 +363,7 @@
       ETAbs e s ->
         let !e' = go e
         in ETAbs e' s
-      PKVar k (Su m) -> PKVar k (Su (go <$>m))
+      PKVar k tsu su -> PKVar k tsu (mapKVarSubst go su)
       e@EVar{} -> e
       e@ESym{} -> e
       e@ECon{} -> e
@@ -398,7 +402,7 @@
     go e@(ESym _)      = f e
     go e@(ECon _)      = f e
     go e@(EVar _)      = f e
-    go e@(PKVar _ _)   = f e
+    go e@(PKVar {})      = f e
     go (ENeg e)        = f . ENeg =<< go e
     go (PNot p)        = f . PNot =<< go p
     go (ECst e t)      = f . (`ECst` t) =<< go e
@@ -418,10 +422,10 @@
     go (PAnd ps)       = f . PAnd =<< (go `traverse` ps)
     go (POr ps)        = f . POr =<< (go `traverse` ps)
 
-mapKVarSubsts :: Visitable t => (KVar -> Subst -> Subst) -> t -> t
+mapKVarSubsts :: Visitable t => (KVar -> KVarSubst Symbol Symbol -> KVarSubst Symbol Symbol) -> t -> t
 mapKVarSubsts f          = trans txK
   where
-    txK (PKVar k su)   = PKVar k (f k su)
+    txK (PKVar k tsu su)   = PKVar k tsu (f k su)
     txK p              = p
 
 newtype MInt = MInt Integer -- deriving (Eq, NFData)
@@ -464,7 +468,7 @@
       ESym _ -> acc
       ECon _ -> acc
       EVar _ -> acc
-      PKVar k _ -> k : acc
+      PKVar k _ _ -> k : acc
       ENeg e -> go acc e
       PNot p -> go acc p
       ECst e _t -> go acc e
@@ -532,11 +536,15 @@
 type CoSub = M.HashMap Symbol Sort
 
 applyCoSub :: CoSub -> Expr -> Expr
-applyCoSub coSub = mapExprOnExpr fE
+applyCoSub coSub
+   | M.null coSub = id
+   | otherwise = mapExprOnExpr fE
   where
     fE (ECoerc s t e) = ECoerc  (txS s) (txS t) e
     fE (ELam (x,t) e) = ELam (x, txS t)         e
     fE (ECst e t)     = ECst e (txS t)
+    fE (PExist xts p) = PExist (map (fmap txS) xts) (fE p)
+    fE (PAll xts p) = PAll (map (fmap txS) xts) (fE p)
     fE e              = e
     txS               = mapSortOnlyOnce fS
     fS (FObj a)       = {- FObj -} txV a
@@ -558,6 +566,13 @@
 
     fS t              = M.lookupDefault t t coSub
 
+applyCoercion :: Symbol -> Sort -> Sort -> Sort
+applyCoercion a t = mapSortOnlyOnce f
+  where
+    f (FObj b)
+      | a == b    = t
+    f s           = s
+
 ---------------------------------------------------------------------------------
 -- | Visitors over @Sort@
 ---------------------------------------------------------------------------------
@@ -663,3 +678,14 @@
     scVis            = (defaultFolder :: Folder [SymConst] t)  { accExpr = sc }
     sc _ (ESym c)    = [c]
     sc _ _           = []
+
+getConstants' :: Foldable t => t -> [Constant]
+getConstants' = nubOrd . fold cVis () []
+  where
+    cVis           = (defaultFolder :: Folder [Constant] t) { accExpr = ac }
+    ac _ (ECon c)  = [c]
+    ac _ _         = []
+
+-- | getConstants returns both the vanilla constants AND the sym-constants as str-literals
+getConstants :: Foldable t => t -> [Constant]
+getConstants z = nubOrd $ getConstants' z ++ [ L t strSort | SL t <- getSymConsts z]
diff --git a/src/Language/Fixpoint/Utils/Files.hs b/src/Language/Fixpoint/Utils/Files.hs
--- a/src/Language/Fixpoint/Utils/Files.hs
+++ b/src/Language/Fixpoint/Utils/Files.hs
@@ -13,6 +13,7 @@
     Ext (..)
   , extFileName
   , extFileNameR
+  , extFileNameR'
   , tempDirectory
   , tempFileName
   , extModuleName
@@ -158,6 +159,12 @@
 
 extFileNameR     :: Ext -> FilePath -> FilePath
 extFileNameR ext = (`addExtension` extMap ext)
+
+-- | Like 'extFileName' but uses a custom output directory when provided.
+-- When 'Nothing', falls back to the default @.liquid/@ directory behavior.
+extFileNameR' :: Maybe FilePath -> Ext -> FilePath -> FilePath
+extFileNameR' Nothing  e f = extFileName e f
+extFileNameR' (Just d) e f = d </> takeFileName (addExtension f (extMap e))
 
 isExtFile ::  Ext -> FilePath -> Bool
 isExtFile ext = (extMap ext ==) . takeExtension
diff --git a/tests/pos/frac.fq b/tests/pos/frac.fq
new file mode 100644
--- /dev/null
+++ b/tests/pos/frac.fq
@@ -0,0 +1,18 @@
+bind 0 alpha : {v : frac | true}
+bind 1 x : {VV : alpha | []}
+bind 2 y : {VV : alpha | [(VV != 0.0)]}
+
+
+
+constraint:
+  env [0]
+  lhs {v : alpha | (v = 10.0)}
+  rhs {v : alpha | (v < 11.0)}
+  id 1 tag []
+
+
+constraint:
+  env [0;1;2]
+  lhs {v : int | []}
+  rhs {v : int | [(((x / y) * y) = x)]}
+  id 2 tag []
diff --git a/tests/tasty/Arbitrary.hs b/tests/tasty/Arbitrary.hs
--- a/tests/tasty/Arbitrary.hs
+++ b/tests/tasty/Arbitrary.hs
@@ -72,7 +72,7 @@
 subexprs (PImp e0 e1)    = [e0, e1]
 subexprs (PIff e0 e1)    = [e0, e1]
 subexprs (PAtom _ e0 e1) = [e0, e1]
-subexprs (PKVar _ _)     = []
+subexprs (PKVar _ _ _)   = []
 subexprs (PAll _ e)      = [e]
 subexprs (PExist _ e)    = [e]
 subexprs (ECoerc _ _ e)  = [e]
@@ -101,7 +101,7 @@
   , (1, PImp <$> arbitraryExpr' <*> arbitraryExpr')
   , (1, PIff <$> arbitraryExpr' <*> arbitraryExpr')
   , (1, PAtom <$> arbitrary <*> arbitraryExpr' <*> arbitraryExpr')
-  , (1, PKVar <$> arbitrary <*> arbitrary)
+  , (1, PKVar <$> arbitrary <*> pure mempty <*> arbitrary)
   , (1, PAll <$> arbitraryList arbitrary <*> arbitraryExpr')
   , (1, PExist <$> arbitraryList arbitrary <*> arbitraryExpr')
   , (1, ECoerc <$> arbitrary <*> arbitrary <*> arbitraryExpr')
@@ -138,6 +138,16 @@
     l <- vectorOf n arbitrary
     return $ Su $ M.fromList l
   shrink _ = mempty
+
+instance Arbitrary (KVarSubst Symbol Symbol) where
+  arbitrary = do
+    n <- choose (0, 3)
+    l <- vectorOf n arbitrary
+    return $ toKVarSubst $ M.fromList l
+
+instance Arbitrary (M.HashMap Symbol Sort) where
+  arbitrary = M.fromList <$> arbitrary
+  shrink = map M.fromList . shrink . M.toList
 
 -- | This instance only creates `FVar` when they would be in scope from an
 -- enclosing `FAbs`, and does not create `FObj`s
diff --git a/tests/tasty/ParserTests.hs b/tests/tasty/ParserTests.hs
--- a/tests/tasty/ParserTests.hs
+++ b/tests/tasty/ParserTests.hs
@@ -2,7 +2,7 @@
 
 module ParserTests (tests) where
 
-import Language.Fixpoint.Types (showFix)
+import Language.Fixpoint.Types (showpp, showFix)
 import Language.Fixpoint.Parse
 import Test.Tasty
 import Test.Tasty.HUnit
@@ -214,13 +214,16 @@
    --   "PGrad $\"\\\"test\\\" (line 1, column 3)\"  (GradInfo {gsrc = SS {sp_start = \"test\" (line 1, column 3), sp_stop = \"test\" (line 1, column 3)}, gused = Nothing}) (PAnd [])"
 
     , testCase "kvarPred empty" $
-        show (doParse' predP "test" "$foo") @?= "PKVar $\"foo\" "
+        show (doParse' predP "test" "$foo") @?= "PKVar $\"foo\" (fromList []) "
 
     , testCase "kvarPred one" $
-        show (doParse' predP "test" "$foo  [x := 1]") @?= "PKVar $\"foo\" [x:=1]"
+        show (doParse' predP "test" "$foo  [x := 1]") @?= "PKVar $\"foo\" (fromList []) [x:=1]"
 
     , testCase "kvarPred two" $
-        show (doParse' predP "test" "$foo  [x := 1] [ y := true ]") @?= "PKVar $\"foo\" [x:=1][y:=true]"
+        show (doParse' predP "test" "$foo  [x := 1] [ y := true ]") @?= "PKVar $\"foo\" (fromList []) [x:=1][y:=true]"
+
+    , testCase "kvarPred tyvar subst" $
+        showpp (doParse' predP "test" "$foo[@a:=b;c:=d] [x := 1] [ y := true ]") @?= "$foo[@a:=b;c:=d][x:=1][y:=true]"
 
     , testCase "fastIf" $
         show (doParse' predP "test" "if true then true else false" ) @?=
diff --git a/tests/tasty/SimplifyInterpreter.hs b/tests/tasty/SimplifyInterpreter.hs
--- a/tests/tasty/SimplifyInterpreter.hs
+++ b/tests/tasty/SimplifyInterpreter.hs
@@ -4,7 +4,7 @@
 import qualified Data.HashSet as S
 import Language.Fixpoint.Solver.Interpreter (ICtx (..), Knowledge (..))
 import qualified Language.Fixpoint.Solver.Interpreter as Interpreter
-import Language.Fixpoint.Types.Environments (SEnv (..))
+import Language.Fixpoint.Types.Environments (SEnvB (..))
 import Language.Fixpoint.Types.Refinements (Expr)
 
 interpret' :: Expr -> Expr
diff --git a/tests/tasty/SimplifyTests.hs b/tests/tasty/SimplifyTests.hs
--- a/tests/tasty/SimplifyTests.hs
+++ b/tests/tasty/SimplifyTests.hs
@@ -1,7 +1,7 @@
 module SimplifyTests (tests) where
 
 import Arbitrary (subexprs)
-import Language.Fixpoint.Types.Refinements (Bop (Minus), Constant (I), Expr, ExprV (..))
+import Language.Fixpoint.Types.Refinements (Bop (Minus), Constant (I), Expr, ExprBV (..))
 import qualified SimplifyInterpreter
 import qualified SimplifyPLE
 import Test.Tasty
diff --git a/tests/test.hs b/tests/test.hs
--- a/tests/test.hs
+++ b/tests/test.hs
@@ -85,41 +85,48 @@
 combineReporters _ _ = error "combineReporters needs TestReporters"
 
 unitTests :: FilePath -> IO TestTree
-unitTests lfDir
-  = group "Unit" [
-      testGroup "native-pos"       <$> dirTests     nativeCmd   "tests/pos"              skipNativePos  ExitSuccess
-    , testGroup "native-neg"       <$> dirTests     nativeCmd   "tests/neg"              ["float.fq"]  (ExitFailure 1)
-    , testGroup "elim-crash"       <$> dirTests     nativeCmd   "tests/crash"            []            (ExitFailure 1)
-    , testGroup "elim-pos1"        <$> dirTests     elimCmd     "tests/pos"              []             ExitSuccess
-    , testGroup "elim-pos2"        <$> dirTests     elimCmd     "tests/elim"             []             ExitSuccess
-    , testGroup "elim-neg"         <$> dirTests     elimCmd     "tests/neg"              ["float.fq"]  (ExitFailure 1)
-    , testGroup "elim-crash"       <$> dirTests     elimCmd     "tests/crash"            []            (ExitFailure 1)
-    , testGroup "cvc5-pos"         <$> dirTests     cvc5Cmd     "tests/pos"              skipNativePos  ExitSuccess
-    , testGroup "cvc5-spec"        <$> dirTests     cvc5Cmd     "tests/cvc5"             skipNativePos  ExitSuccess
-    , testGroup "proof"            <$> dirTests     elimCmd     "tests/proof"            []             ExitSuccess
-    , testGroup "rankN"            <$> dirTests     elimCmd     "tests/rankNTypes"       []             ExitSuccess
-    , testGroup "horn-pos-el"      <$> dirTests     elimSaveCmd "tests/horn/pos"         []             ExitSuccess
-    , testGroup "horn-pos-cvc5"    <$> dirTests     cvc5Cmd     "tests/horn/pos"         []             ExitSuccess
-    , testGroup "horn-neg-el"      <$> dirTests     elimSaveCmd "tests/horn/neg"         []            (ExitFailure 1)
-    , testGroup "horn-neg-cvc5"    <$> dirTests     cvc5Cmd     "tests/horn/neg"         []            (ExitFailure 1)
-    , testGroup "horn-json-pos-el" <$> dirJsonTests elimCmd     "tests/horn/pos/.liquid" []             ExitSuccess
-    , testGroup "horn-json-neg-el" <$> dirJsonTests elimCmd     "tests/horn/neg/.liquid" []            (ExitFailure 1)
-    , testGroup "horn-smt2-pos-el" <$> dirHornTests elimCmd     "tests/horn/pos/.liquid" []             ExitSuccess
-    , testGroup "horn-smt2-neg-el" <$> dirHornTests elimCmd     "tests/horn/neg/.liquid" []            (ExitFailure 1)
-    , testGroup "horn-pos-na"      <$> dirTests     nativeCmd   "tests/horn/pos"         []             ExitSuccess
-    , testGroup "horn-neg-na"      <$> dirTests     nativeCmd   "tests/horn/neg"         []            (ExitFailure 1)
-   ]
-   where
-    dirTests     = dirTests' isTest
-    dirJsonTests = dirTests' ("horn.json" `isSuffixOf`)
-    dirHornTests = dirTests' ("horn.smt2" `isSuffixOf`)
+unitTests lfDir =
+    group "All"
+      [ group "original"
+        [ dirTests "native-pos"           nativeCmd   "tests/pos"              posOptions skipNativePos  ExitSuccess
+        , dirTests "native-neg"           nativeCmd   "tests/neg"              [] ["float.fq"]  (ExitFailure 1)
+        , dirTests "elim-crash"           nativeCmd   "tests/crash"            posOptions []            (ExitFailure 1)
+        , dirTests "elim-pos1"            elimCmd     "tests/pos"              posOptions []             ExitSuccess
+        , dirTests "elim-pos2"            elimCmd     "tests/elim"             posOptions []             ExitSuccess
+        , dirTests "elim-neg"             elimCmd     "tests/neg"              [] ["float.fq"]  (ExitFailure 1)
+        , dirTests "elim-crash"           elimCmd     "tests/crash"            []                      []            (ExitFailure 1)
+        , dirTests "cvc5-pos"             cvc5Cmd     "tests/pos"              posOptions skipNativePos  ExitSuccess
+        , dirTests "cvc5-spec"            cvc5Cmd     "tests/cvc5"             posOptions skipNativePos  ExitSuccess
+        , dirTests "proof"                elimCmd     "tests/proof"            posOptions []             ExitSuccess
+        , dirTests "rankN"                elimCmd     "tests/rankNTypes"       posOptions []             ExitSuccess
+        , dirTests "horn-pos-el"          elimSaveCmd "tests/horn/pos"         posOptions []             ExitSuccess
+        , dirTests "horn-pos-cvc5"        cvc5Cmd     "tests/horn/pos"         posOptions []             ExitSuccess
+        , dirTests "horn-neg-el"          elimSaveCmd "tests/horn/neg"         []         []            (ExitFailure 1)
+        , dirTests "horn-neg-cvc5"        cvc5Cmd     "tests/horn/neg"         []         []            (ExitFailure 1)
+        , dirTests "horn-pos-na"          nativeCmd   "tests/horn/pos"         posOptions []             ExitSuccess
+        , dirTests "horn-neg-na"          nativeCmd   "tests/horn/neg"         []         []            (ExitFailure 1)
+        ]
+      , after AllSucceed "original" <$> group "saved"
+        [ dirJsonTests "horn-json-pos-el" elimCmd     "tests/logs/cur/horn-pos-el" []         []             ExitSuccess
+        , dirJsonTests "horn-json-neg-el" elimCmd     "tests/logs/cur/horn-neg-el" []         []            (ExitFailure 1)
+        , dirHornTests "horn-smt2-pos-el" elimCmd     "tests/logs/cur/horn-pos-el" []         []             ExitSuccess
+        , dirHornTests "horn-smt2-neg-el" elimCmd     "tests/logs/cur/horn-neg-el" []         []            (ExitFailure 1)
+        ]
+      ]
+  where
+    posOptions = ["--save-bfq-on-error"]
 
-    dirTests' :: (FilePath -> Bool) -> TestCmd -> FilePath -> [FilePath] -> ExitCode -> IO [TestTree]
-    dirTests' isT testCmd root ignored code = do
+    dirTests     n a b c d e = testGroup n <$> dirTests' n isTest a b c d e
+    dirJsonTests n a b c d e = testGroup n <$> dirTests' n ("horn.json" `isSuffixOf`) a b c d e
+    dirHornTests n a b c d e = testGroup n <$> dirTests' n ("horn.smt2" `isSuffixOf`) a b c d e
+
+    dirTests' :: String -> (FilePath -> Bool) -> TestCmd -> FilePath -> [String] -> [FilePath] -> ExitCode -> IO [TestTree]
+    dirTests' testName isT testCmd root extraOpts ignored code = do
       let absRoot = lfDir </> root
       files    <- walkDirectory absRoot
       let tests = [ rel | f <- files, isT f, let rel = makeRelative absRoot f, rel `notElem` ignored ]
-      return    $ mkTest testCmd code absRoot <$> tests
+          saveDir = "--save-dir=" ++ lfDir </> "tests" </> "logs" </> "cur" </> testName
+      return $ mkTest testName testCmd code (saveDir : extraOpts) absRoot <$> tests
 
 isTest   :: FilePath -> Bool
 isTest f = takeExtension f `elem` [".fq", ".smt2"]
@@ -150,9 +157,9 @@
       )
 
 ---------------------------------------------------------------------------
-mkTest :: TestCmd -> ExitCode -> FilePath -> FilePath -> TestTree
+mkTest :: String -> TestCmd -> ExitCode -> [String] -> FilePath -> FilePath -> TestTree
 ---------------------------------------------------------------------------
-mkTest testCmd code dir file
+mkTest testName testCmd code extraOpts dir file
   =
     askOption $ \opts ->
     testCase file $
@@ -163,7 +170,7 @@
       else do
         createDirectoryIfMissing True $ takeDirectory log
         c <- withFile log WriteMode $ \h -> do
-          let cmd     = testCmd opts "fixpoint" dir file
+          let cmd     = testCmd (LO (unwords extraOpts) <> opts) "fixpoint" dir file
           (_,_,_,ph) <- createProcess $ (shell cmd) {std_out = UseHandle h, std_err = UseHandle h}
           waitForProcess ph
         when (code /= c) $
@@ -172,7 +179,9 @@
 
   where
     test = dir </> file
-    log  = let (d,f) = splitFileName file in dir </> d </> ".liquid" </> f <.> "log"
+    -- select a file name that is unique to the test, as the tests might run
+    -- in parallel.
+    log  = let (d,f) = splitFileName file in dir </> d </> ".liquid" </> testName </> f <.> "harness.log"
 
 knownToFail :: [a]
 knownToFail = []
@@ -194,10 +203,6 @@
 cvc5Cmd :: TestCmd
 cvc5Cmd (LO opts) bin dir file =
   printf "cd %s && %s --solver=cvc5 %s %s" dir bin opts file
-
-cvc5SaveCmd :: TestCmd
-cvc5SaveCmd (LO opts) bin dir file =
-  printf "cd %s && %s --save --solver=cvc5 %s %s" dir bin opts file
 
 ----------------------------------------------------------------------------------------
 -- Generic Helpers