diff --git a/CHANGES.md b/CHANGES.md
index a94c8e264..a9cfca8f6 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -2,8 +2,11 @@
 
 ## NEXT
 
+## 0.8.0.1 
+
 - Support for "existential binders", see `tests/pos/ebind-*.fq` for example.
   This only works with `--eliminate`.
+- Move to GHC 8.4.3 
 
 ## 0.7.0.0
 
diff --git a/liquid-fixpoint.cabal b/liquid-fixpoint.cabal
index f7f1bdd77..5106b4a49 100644
--- a/liquid-fixpoint.cabal
+++ b/liquid-fixpoint.cabal
@@ -1,5 +1,5 @@
 name:                liquid-fixpoint
-version:             0.7.0.7
+version:             0.8.0.1
 Copyright:           2010-17 Ranjit Jhala, University of California, San Diego.
 synopsis:            Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
 homepage:            https://github.com/ucsd-progsys/liquid-fixpoint
@@ -53,7 +53,7 @@ Executable fixpoint
   if flag(devel)
     ghc-options: -Werror
   hs-source-dirs: bin
-  Build-Depends: base >=4.8.1.0 && <5
+  Build-Depends: base >=4.9.1.0 && <5
                , liquid-fixpoint
 
 Library
@@ -85,7 +85,6 @@ Library
                    Language.Fixpoint.Graph.Partition,
                    Language.Fixpoint.Graph.Deps,
                    Language.Fixpoint.Graph,
-                   -- Language.Fixpoint.Congruence.Closure,
                    Language.Fixpoint.Defunctionalize,
                    Language.Fixpoint.Smt.Types,
                    Language.Fixpoint.Smt.Bitvector,
@@ -110,9 +109,13 @@ Library
                    Language.Fixpoint.Solver.Instantiate,
                    Language.Fixpoint.Solver.Sanitize,
                    Language.Fixpoint.Utils.Statistics,
-                   Language.Fixpoint.Solver.Solve
+                   Language.Fixpoint.Solver.Solve,
 
-  Build-Depends: base >=4.8.1.0 && <5
+                   Text.PrettyPrint.HughesPJ.Compat
+
+  Other-Modules: Paths_liquid_fixpoint
+
+  Build-Depends: base >=4.9.1.0 && <5
                , array
                , async
                , attoparsec
@@ -131,7 +134,7 @@ Library
                , intern
                , mtl
                , parsec
-               , pretty
+               , pretty >=1.1.3.1
                , boxes
                , parallel
                , process
@@ -148,8 +151,9 @@ Library
                , time
                , parallel-io
 
-  if impl(ghc >= 7.10.2)
-    Build-Depends: located-base
+  -- unconditionally depend on located-base
+  Build-Depends: located-base
+
   if !os(windows)
     Build-Depends: ascii-progress >= 0.3
     hs-source-dirs: unix
@@ -164,21 +168,23 @@ test-suite test
   if flag(devel)
     ghc-options:    -Werror
   main-is:          test.hs
-  build-depends:    base >= 4.8 && < 5,
+  Other-Modules:    Paths_liquid_fixpoint
+  build-depends:    base >= 4.9.1.0 && < 5,
                     directory,
                     filepath,
                     process,
                     stm >= 2.4,
                     containers >= 0.5,
-                    mtl >= 2.1,
-                    transformers >= 0.3,
+                    mtl >= 2.2.2,
+                    transformers >= 0.5,
                     tasty >= 0.10,
                     tasty-hunit,
-                    tasty-rerun >= 1.1,
+                    tasty-rerun >= 1.1.12,
                     tasty-ant-xml,
                     tasty-hunit >= 0.9,
                     text
 
+
 test-suite testparser
   default-language: Haskell98
   type:             exitcode-stdio-1.0
@@ -187,7 +193,7 @@ test-suite testparser
   if flag(devel)
     ghc-options:    -Werror
   main-is:          testParser.hs
-  build-depends:    base >= 4.8 && < 5,
+  build-depends:    base >= 4.9.1.0 && < 5,
                     directory,
                     filepath,
                     tasty >= 0.10,
@@ -195,9 +201,32 @@ test-suite testparser
                     tasty-rerun >= 1.1,
                     tasty-ant-xml,
                     tasty-hunit >= 0.9,
-                    text
+                    text,
+                    liquid-fixpoint
   if flag(devel)
     hs-source-dirs:   tests src
+    other-modules:
+                 Language.Fixpoint.Misc
+                 Language.Fixpoint.Parse
+                 Language.Fixpoint.Smt.Bitvector
+                 Language.Fixpoint.Smt.Types
+                 Language.Fixpoint.Types
+                 Language.Fixpoint.Types.Config
+                 Language.Fixpoint.Types.Constraints
+                 Language.Fixpoint.Types.Environments
+                 Language.Fixpoint.Types.Errors
+                 Language.Fixpoint.Types.Names
+                 Language.Fixpoint.Types.PrettyPrint
+                 Language.Fixpoint.Types.Refinements
+                 Language.Fixpoint.Types.Sorts
+                 Language.Fixpoint.Types.Spans
+                 Language.Fixpoint.Types.Substitutions
+                 Language.Fixpoint.Types.Theories
+                 Language.Fixpoint.Types.Triggers
+                 Language.Fixpoint.Types.Utils
+                 Language.Fixpoint.Utils.Files
+                 Text.PrettyPrint.HughesPJ.Compat
+
     build-depends:
                  array
                , async
diff --git a/src/Language/Fixpoint/Graph/Deps.hs b/src/Language/Fixpoint/Graph/Deps.hs
index 6ed5819e3..aa789478e 100644
--- a/src/Language/Fixpoint/Graph/Deps.hs
+++ b/src/Language/Fixpoint/Graph/Deps.hs
@@ -28,6 +28,7 @@ module Language.Fixpoint.Graph.Deps (
 
 import           Prelude hiding (init)
 import           Data.Maybe                       (mapMaybe, fromMaybe)
+import           Data.Semigroup                   (Semigroup (..))
 import           Data.Tree (flatten)
 import           Language.Fixpoint.Misc
 import           Language.Fixpoint.Utils.Files
@@ -46,7 +47,7 @@ import qualified Data.HashMap.Strict                  as M
 import qualified Data.Graph                           as G
 import           Data.Function (on)
 import           Data.Hashable
-import           Text.PrettyPrint.HughesPJ
+import           Text.PrettyPrint.HughesPJ.Compat
 import           Debug.Trace (trace)
 
 --------------------------------------------------------------------------------
@@ -289,9 +290,12 @@ instance PPrint (Elims a) where
     where
       ppSize     = pprint . S.size
 
+instance (Eq a, Hashable a) => Semigroup (Elims a) where
+  Deps d1 n1 <> Deps d2 n2 = Deps (S.union d1 d2) (S.union n1 n2)
+
 instance (Eq a, Hashable a) => Monoid (Elims a) where
-  mempty                            = Deps S.empty S.empty
-  mappend (Deps d1 n1) (Deps d2 n2) = Deps (S.union d1 d2) (S.union n1 n2)
+  mempty  = Deps S.empty S.empty
+  mappend = (<>)
 
 dCut, dNonCut :: (Hashable a) => a -> Elims a
 dNonCut v = Deps S.empty (S.singleton v)
@@ -551,7 +555,7 @@ instance PTable Stats where
 
 graphStats :: F.TaggedC c a => Config -> F.GInfo c a -> Stats
 graphStats cfg si = Stats {
-    stNumKVCuts   = S.size $ F.tracepp "CUTS:" (depCuts d)
+    stNumKVCuts   = S.size (depCuts d)
   , stNumKVNonLin = S.size  nlks
   , stNumKVTotal  = S.size (depCuts d) + S.size (depNonCuts d)
   , stIsReducible = isReducible si
diff --git a/src/Language/Fixpoint/Graph/Partition.hs b/src/Language/Fixpoint/Graph/Partition.hs
index 1fa677028..6e2975385 100644
--- a/src/Language/Fixpoint/Graph/Partition.hs
+++ b/src/Language/Fixpoint/Graph/Partition.hs
@@ -38,7 +38,8 @@ import qualified Data.HashMap.Strict                  as M
 -- import           Data.Function (on)
 import           Data.Maybe                     (fromMaybe)
 import           Data.Hashable
-import           Text.PrettyPrint.HughesPJ
+import           Data.Semigroup                 (Semigroup (..))
+import           Text.PrettyPrint.HughesPJ.Compat
 import           Data.List (sortBy)
 -- import qualified Data.HashSet              as S
 
@@ -55,12 +56,15 @@ data CPart c a = CPart { pws :: !(M.HashMap F.KVar (F.WfC a))
                        , pcm :: !(M.HashMap Integer (c a))
                        }
   
+instance Semigroup (CPart c a) where
+  l <> r = CPart { pws = pws l <> pws r
+                 , pcm = pcm l <> pcm r
+                 }
+
 instance Monoid (CPart c a) where
    mempty      = CPart mempty mempty
-   mappend l r = CPart { pws = pws l `mappend` pws r
-                       , pcm = pcm l `mappend` pcm r
-                       }
-
+   mappend     = (<>)
+   
 --------------------------------------------------------------------------------
 -- | Multicore info ------------------------------------------------------------
 --------------------------------------------------------------------------------
diff --git a/src/Language/Fixpoint/Graph/Types.hs b/src/Language/Fixpoint/Graph/Types.hs
index 8ca5056dc..ef2b12c65 100644
--- a/src/Language/Fixpoint/Graph/Types.hs
+++ b/src/Language/Fixpoint/Graph/Types.hs
@@ -50,7 +50,7 @@ module Language.Fixpoint.Graph.Types (
 
 import           GHC.Generics              (Generic)
 import           Data.Hashable
-import           Text.PrettyPrint.HughesPJ
+import           Text.PrettyPrint.HughesPJ.Compat
 
 import           Language.Fixpoint.Misc         -- hiding (group)
 import           Language.Fixpoint.Types.PrettyPrint
@@ -73,8 +73,8 @@ data CVertex = KVar  !KVar    -- ^ real kvar vertex
 instance PPrint CVertex where
   pprintTidy _ (KVar k)  = doubleQuotes $ pprint $ kv k
   pprintTidy _ (EBind s)  = doubleQuotes $ pprint $ s
-  pprintTidy _ (Cstr i)  = text "id_" <> pprint i
-  pprintTidy _ (DKVar k) = pprint k   <> text "*"
+  pprintTidy _ (Cstr i)  = text "id_" <-> pprint i
+  pprintTidy _ (DKVar k) = pprint k   <-> text "*"
 
 
 instance Hashable CVertex
diff --git a/src/Language/Fixpoint/Misc.hs b/src/Language/Fixpoint/Misc.hs
index b48c627c0..3504a2eae 100644
--- a/src/Language/Fixpoint/Misc.hs
+++ b/src/Language/Fixpoint/Misc.hs
@@ -18,12 +18,14 @@ import           Control.Arrow                    (second)
 import           Control.Monad                    (when, forM_, filterM)
 import qualified Data.HashMap.Strict              as M
 import qualified Data.List                        as L
+import qualified Data.HashSet                     as S
 import           Data.Tuple                       (swap)
 import           Data.Maybe
 import           Data.Array                       hiding (indices)
 import           Data.Function                    (on)
 import qualified Data.Graph                       as G
 import qualified Data.Tree                        as T
+
 import           Data.Unique
 import           Debug.Trace                      (trace)
 import           System.Console.ANSI
@@ -31,17 +33,13 @@ import           System.Console.CmdArgs.Verbosity (whenLoud)
 import           System.Process                   (system)
 import           System.Directory                 (createDirectoryIfMissing)
 import           System.FilePath                  (takeDirectory)
-import           Text.PrettyPrint.HughesPJ        hiding (first)
+import           Text.PrettyPrint.HughesPJ.Compat
 import           System.IO                        (stdout, hFlush )
 import           System.Exit                      (ExitCode)
 import           Control.Concurrent.Async
 
-
-#ifdef MIN_VERSION_located_base
-import Prelude hiding (error, undefined)
-import GHC.Err.Located
+import Prelude hiding (undefined)
 import GHC.Stack
-#endif
 
 type (|->) a b = M.HashMap a b
 
@@ -58,6 +56,15 @@ traceShow s x = trace ("\nTrace: [" ++ s ++ "] : " ++ show x)  x
 hashMapToAscList :: Ord a => M.HashMap a b -> [(a, b)]
 hashMapToAscList = L.sortBy (compare `on` fst) . M.toList
 
+findNearest :: (Ord i, Num i) => i -> [(i, a)] -> Maybe a 
+findNearest key kvs = argMin [ (abs (key - k), v) | (k, v) <- kvs ]
+
+argMin :: (Ord k) => [(k, v)] -> Maybe v 
+argMin = fmap snd . headMb . L.sortBy (compare `on` fst)
+
+headMb :: [a] -> Maybe a 
+headMb []    = Nothing 
+headMb (x:_) = Just x
 ---------------------------------------------------------------
 -- | Unique Int -----------------------------------------------
 ---------------------------------------------------------------
@@ -139,10 +146,11 @@ wrap l r s = l ++ s ++ r
 repeats :: Int -> [a] -> [a]
 repeats n  = concat . replicate n
 
-#ifdef MIN_VERSION_located_base
-errorstar :: (?callStack :: CallStack) => String -> a
-#endif
 
+errorP :: String -> String -> a
+errorP p s = error (p ++ s)   
+
+errorstar :: (?callStack :: CallStack) => String -> a
 errorstar  = error . wrap (stars ++ "\n") (stars ++ "\n")
   where
     stars = repeats 3 $ wrapStars "ERROR"
@@ -159,15 +167,9 @@ thd3 (_,_,x) = x
 secondM :: Functor f => (b -> f c) -> (a, b) -> f (a, c)
 secondM act (x, y) = (x,) <$> act y
 
-#ifdef MIN_VERSION_located_base
 mlookup    :: (?callStack :: CallStack, Eq k, Show k, Hashable k) => M.HashMap k v -> k -> v
 safeLookup :: (?callStack :: CallStack, Eq k, Hashable k) => String -> k -> M.HashMap k v -> v
 mfromJust  :: (?callStack :: CallStack) => String -> Maybe a -> a
-#else
-mlookup    :: (Eq k, Show k, Hashable k) => M.HashMap k v -> k -> v
-safeLookup :: (Eq k, Hashable k) => String -> k -> M.HashMap k v -> v
-mfromJust  :: String -> Maybe a -> a
-#endif
 
 mlookup m k = fromMaybe err $ M.lookup k m
   where
@@ -206,19 +208,21 @@ hashNub = M.keys . M.fromList . fmap (, ())
 
 sortNub :: (Ord a) => [a] -> [a]
 sortNub = nubOrd . L.sort
-  where
-    nubOrd (x:t@(y:_))
-      | x == y    = nubOrd t
-      | otherwise = x : nubOrd t
-    nubOrd xs     = xs
+
+nubOrd :: (Eq a) => [a] -> [a]
+nubOrd (x:t@(y:_))
+  | x == y    = nubOrd t
+  | otherwise = x : nubOrd t
+nubOrd xs     = xs
+
+hashNubWith :: (Eq b, Hashable b) => (a -> b) -> [a] -> [a]
+hashNubWith f xs = M.elems $ M.fromList [ (f x, x) | x <- xs ]
 
 duplicates :: (Eq k, Hashable k) => [k] -> [k]
 duplicates xs = [ x | (x, n) <- count xs, 1 < n ]
 
-#ifdef MIN_VERSION_located_base
 safeZip :: (?callStack :: CallStack) => String -> [a] -> [b] -> [(a,b)]
 safeZipWith :: (?callStack :: CallStack) => String -> (a -> b -> c) -> [a] -> [b] -> [c]
-#endif
 
 safeZip msg xs ys
   | nxs == nys
@@ -241,21 +245,12 @@ safeZipWith msg f xs ys
 {-@ type ListNE a = {v:[a] | 0 < len v} @-}
 type ListNE a = [a]
 
-#ifdef MIN_VERSION_located_base
 safeHead   :: (?callStack :: CallStack) => String -> ListNE a -> a
 safeLast   :: (?callStack :: CallStack) => String -> ListNE a -> a
 safeInit   :: (?callStack :: CallStack) => String -> ListNE a -> [a]
 safeUncons :: (?callStack :: CallStack) => String -> ListNE a -> (a, [a])
 safeUnsnoc :: (?callStack :: CallStack) => String -> ListNE a -> ([a], a)
 safeFromList :: (?callStack :: CallStack, Eq k, Hashable k, Show k) => String -> [(k, v)] -> M.HashMap k v
-#else
-safeHead   :: String -> ListNE a -> a
-safeLast   :: String -> ListNE a -> a
-safeInit   :: String -> ListNE a -> [a]
-safeUncons :: String -> ListNE a -> (a, [a])
-safeUnsnoc :: String -> ListNE a -> ([a], a)
-safeFromList :: (Eq k, Hashable k, Show k) => String -> [(k, v)] -> M.HashMap k v
-#endif
 
 safeFromList msg kvs = applyNonNull (M.fromList kvs) err (dups kvs)
   where
@@ -288,7 +283,7 @@ applyNonNull _   f xs = f xs
 
 arrow, dcolon :: Doc
 arrow              = text "->"
-dcolon             = colon <> colon
+dcolon             = colon <-> colon
 
 intersperse :: Doc -> [Doc] -> Doc
 intersperse d ds   = hsep $ punctuate d ds
@@ -334,6 +329,10 @@ mapEither f (x:xs) = case f x of
                      where
                        (ys, zs) = mapEither f xs
 
+isRight :: Either a b -> Bool 
+isRight (Right _) = True 
+isRight _         = False
+
 componentsWith :: (Ord c) => (a -> [(b, c, [c])]) -> a -> [[b]]
 componentsWith eF x = map (fst3 . f) <$> vss
   where
@@ -436,3 +435,10 @@ revMapM f          = go []
   where
     go !acc []     = return (reverse acc)
     go !acc (x:xs) = do {!y <- f x; go (y:acc) xs}
+
+-- Null if first is a subset of second
+nubDiff :: (Eq a, Hashable a) => [a] -> [a] -> S.HashSet a 
+nubDiff a b = a' `S.difference` b'
+  where
+    a' = S.fromList a
+    b' = S.fromList b
\ No newline at end of file
diff --git a/src/Language/Fixpoint/Smt/Interface.hs b/src/Language/Fixpoint/Smt/Interface.hs
index eec3c0e3d..9055e1034 100644
--- a/src/Language/Fixpoint/Smt/Interface.hs
+++ b/src/Language/Fixpoint/Smt/Interface.hs
@@ -78,8 +78,8 @@ import           Control.Monad
 import           Control.Exception
 import           Data.Char
 import qualified Data.HashMap.Strict      as M
-import           Data.Monoid
-import           Data.Maybe                  (fromMaybe)
+import           Data.Maybe              (fromMaybe)
+import           Data.Semigroup          (Semigroup (..))
 import qualified Data.Text                as T
 import           Data.Text.Format
 import qualified Data.Text.IO             as TIO
diff --git a/src/Language/Fixpoint/Smt/Serialize.hs b/src/Language/Fixpoint/Smt/Serialize.hs
index bd86c6d22..129e2f8c5 100644
--- a/src/Language/Fixpoint/Smt/Serialize.hs
+++ b/src/Language/Fixpoint/Smt/Serialize.hs
@@ -17,7 +17,7 @@ import           Language.Fixpoint.Types
 import qualified Language.Fixpoint.Types.Visitor as Vis
 import           Language.Fixpoint.Smt.Types
 import qualified Language.Fixpoint.Smt.Theories as Thy
-import           Data.Monoid
+import           Data.Semigroup                 (Semigroup (..))
 import qualified Data.Text.Lazy.Builder         as Builder
 import           Data.Text.Format
 import           Language.Fixpoint.Misc (sortNub, errorstar)
diff --git a/src/Language/Fixpoint/Smt/Theories.hs b/src/Language/Fixpoint/Smt/Theories.hs
index 6c8f06413..bac2106f8 100644
--- a/src/Language/Fixpoint/Smt/Theories.hs
+++ b/src/Language/Fixpoint/Smt/Theories.hs
@@ -37,13 +37,13 @@ module Language.Fixpoint.Smt.Theories
      ) where
 
 import           Prelude hiding (map)
+import           Data.Semigroup            (Semigroup (..))
 import           Language.Fixpoint.Types.Sorts
 import           Language.Fixpoint.Types.Config
 import           Language.Fixpoint.Types
 import           Language.Fixpoint.Smt.Types
 -- import qualified Data.HashMap.Strict      as M
 import           Data.Maybe (catMaybes)
-import           Data.Monoid
 import qualified Data.Text.Lazy           as T
 import qualified Data.Text.Lazy.Builder   as Builder
 import           Data.Text.Format
diff --git a/src/Language/Fixpoint/Solver.hs b/src/Language/Fixpoint/Solver.hs
index 4a6cf2bea..783bb4d5e 100644
--- a/src/Language/Fixpoint/Solver.hs
+++ b/src/Language/Fixpoint/Solver.hs
@@ -205,6 +205,7 @@ simplifyFInfo !cfg !fi0 = do
   loudDump 3 cfg si5
   instantiate cfg $!! si5
 
+
 solveNative' !cfg !fi0 = do
   si6 <- simplifyFInfo cfg fi0
   res <- {-# SCC "Sol.solve" #-} Sol.solve cfg $!! si6
diff --git a/src/Language/Fixpoint/Solver/Sanitize.hs b/src/Language/Fixpoint/Solver/Sanitize.hs
index b62eb4e5b..cf75e865f 100644
--- a/src/Language/Fixpoint/Solver/Sanitize.hs
+++ b/src/Language/Fixpoint/Solver/Sanitize.hs
@@ -241,11 +241,10 @@ cNoFreeVars :: F.SInfo a -> (F.Symbol -> Bool) -> F.SimpC a -> Maybe [F.Symbol]
 cNoFreeVars fi known c = if S.null fv then Nothing else Just (S.toList fv)
   where
     be   = F.bs fi
-    -- lits = fst <$> F.toListSEnv (F.gLits fi)
     ids  = F.elemsIBindEnv $ F.senv c
     cDom = [fst $ F.lookupBindEnv i be | i <- ids]
     cRng = concat [S.toList . F.reftFreeVars . F.sr_reft . snd $ F.lookupBindEnv i be | i <- ids]
-    fv   = (`nubDiff` cDom) . filter (not . known) $ cRng -- `nubDiff` (lits ++ cDom ++ prims fi)
+    fv   = (`Misc.nubDiff` cDom) . filter (not . known) $ cRng 
 
 badCs :: Misc.ListNE (F.SimpC a, [F.Symbol]) -> E.Error
 badCs = E.catErrors . map (E.errFreeVarInConstraint . Misc.mapFst F.subcId)
@@ -258,20 +257,15 @@ banQualifFreeVars :: F.SInfo a -> SanitizeM (F.SInfo a)
 --------------------------------------------------------------------------------
 banQualifFreeVars fi = Misc.applyNonNull (Right fi) (Left . badQuals) bads
   where
-    bads   = [ (q, xs) | q <- F.quals fi, let xs = free q, not (null xs) ]
-    lits   = fst <$> F.toListSEnv (F.gLits fi)
-    free q = S.toList $ F.syms (F.qBody q) `nubDiff` (lits ++ F.prims ++ F.syms (F.qpSym <$> F.qParams q))
-
+    bads    = [ (q, xs) | q <- F.quals fi, let xs = free q, not (null xs) ]
+    free q  = filter (not . isLit) (F.syms q) 
+    isLit x = F.memberSEnv x (F.gLits fi) 
+    -- lits    = fst <$> F.toListSEnv (F.gLits fi)
+    -- free q  = S.toList $ F.syms (F.qBody q) `nubDiff` (lits ++ F.prims ++ F.syms (F.qpSym <$> F.qParams q))
 
 badQuals     :: Misc.ListNE (F.Qualifier, Misc.ListNE F.Symbol) -> E.Error
 badQuals bqs = E.catErrors [ E.errFreeVarInQual q xs | (q, xs) <- bqs]
 
--- Null if first is a subset of second
-nubDiff :: [F.Symbol] -> [F.Symbol] -> S.HashSet F.Symbol
-nubDiff a b = a' `S.difference` b'
-  where
-    a' = S.fromList a
-    b' = S.fromList b
 
 --------------------------------------------------------------------------------
 -- | check that each constraint has RHS of form [k1,...,kn] or [p]
@@ -315,7 +309,8 @@ symbolSorts' cfg fi  = (normalize . compact . (defs ++)) =<< bindSorts fi
     normalize       = fmap (map (unShadow txFun dm))
     dm              = M.fromList defs
     defs            = F.toListSEnv . F.gLits $ fi
-    txFun
+    txFun           
+      | True        = id
       | allowHO cfg = id
       | otherwise   = defuncSort
 
diff --git a/src/Language/Fixpoint/Solver/Solution.hs b/src/Language/Fixpoint/Solver/Solution.hs
index 77d057b89..9c6bb3f1c 100644
--- a/src/Language/Fixpoint/Solver/Solution.hs
+++ b/src/Language/Fixpoint/Solver/Solution.hs
@@ -19,7 +19,7 @@ import qualified Data.HashSet                   as S
 import qualified Data.HashMap.Strict            as M
 import qualified Data.List                      as L
 import           Data.Maybe                     (fromMaybe, maybeToList, isNothing)
-import           Data.Monoid                    ((<>))
+import           Data.Semigroup                 (Semigroup (..))
 import           Language.Fixpoint.Types.PrettyPrint ()
 import           Language.Fixpoint.Types.Visitor      as V
 import qualified Language.Fixpoint.SortCheck          as So
@@ -414,13 +414,16 @@ data KInfo = KI { kiTags  :: [Tag]
                 , kiCubes :: !Integer
                 } deriving (Eq, Ord, Show)
 
-instance Monoid KInfo where
-  mempty         = KI [] 0 1
-  mappend ki ki' = KI ts d s
+instance Semigroup KInfo where
+  ki <> ki' = KI ts d s
     where
-      ts         = appendTags (kiTags  ki) (kiTags  ki')
-      d          = max        (kiDepth ki) (kiDepth ki')
-      s          = (*)        (kiCubes ki) (kiCubes ki')
+      ts    = appendTags (kiTags  ki) (kiTags  ki')
+      d     = max        (kiDepth ki) (kiDepth ki')
+      s     = (*)        (kiCubes ki) (kiCubes ki')
+
+instance Monoid KInfo where
+  mempty  = KI [] 0 1
+  mappend = (<>)
 
 mplus :: KInfo -> KInfo -> KInfo
 mplus ki ki' = (mappend ki ki') { kiCubes = kiCubes ki + kiCubes ki'}
diff --git a/src/Language/Fixpoint/SortCheck.hs b/src/Language/Fixpoint/SortCheck.hs
index 33d920f87..3cfb2933a 100644
--- a/src/Language/Fixpoint/SortCheck.hs
+++ b/src/Language/Fixpoint/SortCheck.hs
@@ -60,13 +60,14 @@ import           Control.Monad.State.Strict
 import qualified Data.HashMap.Strict       as M
 import qualified Data.List                 as L
 import           Data.Maybe                (mapMaybe, fromMaybe, catMaybes)
+import           Data.Semigroup            (Semigroup (..))
 
 import           Language.Fixpoint.Types.PrettyPrint
 import           Language.Fixpoint.Misc
 import           Language.Fixpoint.Types hiding   (subst)
 import qualified Language.Fixpoint.Types.Visitor  as Vis
 import qualified Language.Fixpoint.Smt.Theories   as Thy
-import           Text.PrettyPrint.HughesPJ
+import           Text.PrettyPrint.HughesPJ.Compat
 import           Text.Printf
 
 -- import Debug.Trace
@@ -1035,9 +1036,12 @@ checkFunSort t             = throwErrorAt (errNonFunction 1 t)
 
 newtype TVSubst = Th (M.HashMap Int Sort) deriving (Show)
 
+instance Semigroup TVSubst where
+  (Th s1) <> (Th s2) = Th (s1 <> s2)
+
 instance Monoid TVSubst where
-  mempty                  = Th mempty
-  mappend (Th s1) (Th s2) = Th (mappend s1 s2)
+  mempty  = Th mempty
+  mappend = (<>)
 
 lookupVar :: Int -> TVSubst -> Maybe Sort
 lookupVar i (Th m)   = M.lookup i m
diff --git a/src/Language/Fixpoint/Types/Constraints.hs b/src/Language/Fixpoint/Types/Constraints.hs
index 9607ccf98..0d3895c48 100644
--- a/src/Language/Fixpoint/Types/Constraints.hs
+++ b/src/Language/Fixpoint/Types/Constraints.hs
@@ -83,6 +83,7 @@ module Language.Fixpoint.Types.Constraints (
 
 import qualified Data.Binary as B
 import           Data.Generics             (Data)
+import           Data.Semigroup            (Semigroup (..))
 import           Data.Typeable             (Typeable)
 import           GHC.Generics              (Generic)
 import qualified Data.List                 as L -- (sort, nub, delete)
@@ -102,7 +103,7 @@ import           Language.Fixpoint.Types.Environments
 import qualified Language.Fixpoint.Utils.Files as Files
 
 import           Language.Fixpoint.Misc
-import           Text.PrettyPrint.HughesPJ
+import           Text.PrettyPrint.HughesPJ.Compat
 import qualified Data.HashMap.Strict       as M
 import qualified Data.HashSet              as S
 
@@ -250,8 +251,9 @@ subcId = mfromJust "subCId" . sid
 type GFixSolution = GFixSol Expr
 
 type FixSolution  = M.HashMap KVar Expr
+
 newtype GFixSol e = GSol (M.HashMap KVar (e, [e]))
-  deriving (Generic, Monoid, Functor)
+  deriving (Generic, Semigroup, Monoid, Functor)
 
 toGFixSol :: M.HashMap KVar (e, [e]) -> GFixSol e
 toGFixSol = GSol
@@ -262,13 +264,16 @@ data Result a = Result { resStatus    :: !(FixResult a)
                        , gresSolution :: !GFixSolution }
                 deriving (Generic, Show)
 
+instance Semigroup (Result a) where
+  r1 <> r2  = Result stat soln gsoln
+    where
+      stat  = (resStatus r1)    <> (resStatus r2)
+      soln  = (resSolution r1)  <> (resSolution r2)
+      gsoln = (gresSolution r1) <> (gresSolution r2)
+
 instance Monoid (Result a) where
   mempty        = Result mempty mempty mempty
-  mappend r1 r2 = Result stat soln gsoln
-    where
-      stat      = mappend (resStatus r1)    (resStatus r2)
-      soln      = mappend (resSolution r1)  (resSolution r2)
-      gsoln     = mappend (gresSolution r1) (gresSolution r2)
+  mappend       = (<>)
 
 unsafe, safe :: Result a
 unsafe = mempty {resStatus = Unsafe []}
@@ -290,7 +295,7 @@ instance (Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a)) where
   toFix (Unsafe xs)      = vcat $ text "Unsafe:" : pprSinfos "WARNING: " xs
 
 pprSinfos :: (Ord a, Fixpoint a) => String -> [SubC a] -> [Doc]
-pprSinfos msg = map ((text msg <>) . toFix) . L.sort . fmap sinfo
+pprSinfos msg = map ((text msg <->) . toFix) . L.sort . fmap sinfo
 
 instance Fixpoint a => Show (WfC a) where
   show = showFix
@@ -345,7 +350,7 @@ instance PPrint GFixSolution where
   pprintTidy k (GSol xs) = vcat $ punctuate "\n\n" (pprintTidyGradual k <$> M.toList xs)
 
 pprintTidyGradual :: Tidy -> (KVar, (Expr, [Expr])) -> Doc
-pprintTidyGradual _ (x, (e, es)) = ppLocOfKVar x <+> text ":=" <+> (ppNonTauto " && " e <> pprint es)
+pprintTidyGradual _ (x, (e, es)) = ppLocOfKVar x <+> text ":=" <+> (ppNonTauto " && " e <-> pprint es)
 
 ppLocOfKVar :: KVar -> Doc
 ppLocOfKVar = text. dropWhile (/='(') . symbolString .kv
@@ -353,7 +358,7 @@ ppLocOfKVar = text. dropWhile (/='(') . symbolString .kv
 ppNonTauto :: Doc -> Expr -> Doc
 ppNonTauto d e
   | isTautoPred e = mempty
-  | otherwise     = pprint e <> d
+  | otherwise     = pprint e <-> d
 
 instance Show   GFixSolution where
   show = showpp
@@ -472,6 +477,20 @@ instance Loc Qualifier where
     where
       l     = qPos q
 
+instance Subable Qualifier where 
+  syms   = qualFreeSymbols 
+  subst  = mapQualBody . subst
+  substf = mapQualBody . substf
+  substa = mapQualBody . substa
+
+mapQualBody :: (Expr -> Expr) -> Qualifier -> Qualifier
+mapQualBody f q = q { qBody = f (qBody q) }
+  
+qualFreeSymbols :: Qualifier -> [Symbol]
+qualFreeSymbols q = filter (not . isPrim) xs 
+  where
+    xs            = syms (qBody q) L.\\ syms (qpSym <$> qParams q) 
+
 instance Fixpoint QualParam where 
   toFix (QP x _ t) = toFix (x, t) 
 
@@ -480,8 +499,8 @@ instance PPrint QualParam where
 
 instance PPrint QualPattern where 
   pprintTidy _ PatNone         = "" 
-  pprintTidy k (PatPrefix s i) = "as" <+> pprintTidy k s <+> ("$" <> pprint i)
-  pprintTidy k (PatSuffix s i) = "as" <+> ("$" <> pprint i) <+> pprintTidy k s 
+  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 
 
 instance Fixpoint Qualifier where
@@ -491,7 +510,7 @@ instance PPrint Qualifier where
   pprintTidy k q = "qualif" <+> pprintTidy k (qName q) <+> "defined at" <+> pprintTidy k (qPos q)
 
 pprQual :: Qualifier -> Doc
-pprQual (Q n xts p l) = text "qualif" <+> text (symbolString n) <> parens args <> colon <+> parens (toFix p) <+> text "//" <+> toFix l
+pprQual (Q n xts p l) = text "qualif" <+> text (symbolString n) <-> parens args <-> colon <+> parens (toFix p) <+> text "//" <+> toFix l
   where
     args              = intersperse comma (toFix <$> xts)
 
@@ -576,14 +595,17 @@ newtype Kuts = KS { ksVars :: S.HashSet KVar }
                deriving (Eq, Show, Generic)
 
 instance Fixpoint Kuts where
-  toFix (KS s) = vcat $ ((text "cut " <>) . toFix) <$> S.toList s
+  toFix (KS s) = vcat $ (("cut " <->) . toFix) <$> S.toList s
 
 ksMember :: KVar -> Kuts -> Bool
 ksMember k (KS s) = S.member k s
 
+instance Semigroup Kuts where
+  k1 <> k2 = KS $ S.union (ksVars k1) (ksVars k2)
+
 instance Monoid Kuts where
-  mempty        = KS S.empty
-  mappend k1 k2 = KS $ S.union (ksVars k1) (ksVars k2)
+  mempty  = KS S.empty
+  mappend = (<>)
 
 ------------------------------------------------------------------------
 -- | Constructing Queries
@@ -661,11 +683,30 @@ data GInfo c a =
 instance HasGradual (GInfo c a) where
   isGradual info = any isGradual (M.elems $ ws info)
 
+instance Semigroup HOInfo where
+  i1 <> i2 = HOI { hoBinds = hoBinds i1 || hoBinds i2
+                 , hoQuals = hoQuals i1 || hoQuals i2
+                 }
+
 instance Monoid HOInfo where
   mempty        = HOI False False
-  mappend i1 i2 = HOI { hoBinds = hoBinds i1 || hoBinds i2
-                      , hoQuals = hoQuals i1 || hoQuals i2
-                      }
+
+instance Semigroup (GInfo c a) where
+  i1 <> i2 = FI { cm       = (cm i1)       <> (cm i2)
+                , ws       = (ws i1)       <> (ws i2)
+                , bs       = (bs i1)       <> (bs i2)
+                , ebinds   = (ebinds i1)   <> (ebinds i2)
+                , gLits    = (gLits i1)    <> (gLits i2)
+                , dLits    = (dLits i1)    <> (dLits i2)
+                , kuts     = (kuts i1)     <> (kuts i2)
+                , quals    = (quals i1)    <> (quals i2)
+                , bindInfo = (bindInfo i1) <> (bindInfo i2)
+                , ddecls   = (ddecls i1)   <> (ddecls i2)
+                , hoInfo   = (hoInfo i1)   <> (hoInfo i2)
+                , asserts  = (asserts i1)  <> (asserts i2)
+                , ae       = (ae i1)       <> (ae i2)
+                }
+
 
 instance Monoid (GInfo c a) where
   mempty        = FI { cm       = M.empty
@@ -683,21 +724,6 @@ instance Monoid (GInfo c a) where
                      , ae       = mempty
                      } 
 
-  mappend i1 i2 = FI { cm       = mappend (cm i1)       (cm i2)
-                     , ws       = mappend (ws i1)       (ws i2)
-                     , bs       = mappend (bs i1)       (bs i2)
-                     , ebinds   = mappend (ebinds i1)   (ebinds i2)
-                     , gLits    = mappend (gLits i1)    (gLits i2)
-                     , dLits    = mappend (dLits i1)    (dLits i2)
-                     , kuts     = mappend (kuts i1)     (kuts i2)
-                     , quals    = mappend (quals i1)    (quals i2)
-                     , bindInfo = mappend (bindInfo i1) (bindInfo i2)
-                     , ddecls   = mappend (ddecls i1)   (ddecls i2)
-                     , hoInfo   = mappend (hoInfo i1)   (hoInfo i2)
-                     , asserts  = mappend (asserts i1)  (asserts i2)
-                     , ae       = mappend (ae i1)       (ae i2)
-                     }
-
 instance PTable (SInfo a) where
   ptable z = DocTable [ (text "# Sub Constraints", pprint $ length $ cm z)
                       , (text "# WF  Constraints", pprint $ length $ ws z)
@@ -832,13 +858,16 @@ instance NFData Equation
 instance NFData SMTSolver
 instance NFData Eliminate
 
-instance Monoid AxiomEnv where
-  mempty           = AEnv [] [] (M.fromList [])
-  mappend a1 a2    = AEnv aenvEqs' aenvSimpl' aenvExpand'
+instance Semigroup AxiomEnv where
+  a1 <> a2        = AEnv aenvEqs' aenvSimpl' aenvExpand'
     where
-      aenvEqs'     = mappend (aenvEqs a1) (aenvEqs a2)
-      aenvSimpl'   = mappend (aenvSimpl a1) (aenvSimpl a2)
-      aenvExpand'  = mappend (aenvExpand a1) (aenvExpand a2)
+      aenvEqs'    = (aenvEqs a1)    <> (aenvEqs a2)
+      aenvSimpl'  = (aenvSimpl a1)  <> (aenvSimpl a2)
+      aenvExpand' = (aenvExpand a1) <> (aenvExpand a2)
+
+instance Monoid AxiomEnv where
+  mempty          = AEnv [] [] (M.fromList [])
+  mappend         = (<>)
 
 instance PPrint AxiomEnv where
   pprintTidy _ = text . show
diff --git a/src/Language/Fixpoint/Types/Environments.hs b/src/Language/Fixpoint/Types/Environments.hs
index 11108e739..ff323c3cf 100644
--- a/src/Language/Fixpoint/Types/Environments.hs
+++ b/src/Language/Fixpoint/Types/Environments.hs
@@ -60,6 +60,7 @@ module Language.Fixpoint.Types.Environments (
 import qualified Data.Binary as B
 import qualified Data.List   as L
 import           Data.Generics             (Data)
+import           Data.Semigroup            (Semigroup (..))
 import           Data.Typeable             (Typeable)
 import           GHC.Generics              (Generic)
 import           Data.Hashable
@@ -67,7 +68,7 @@ import qualified Data.HashMap.Strict       as M
 import qualified Data.HashSet              as S
 import           Data.Maybe
 import           Data.Function             (on)
-import           Text.PrettyPrint.HughesPJ
+import           Text.PrettyPrint.HughesPJ.Compat
 import           Control.DeepSeq
 
 import           Language.Fixpoint.Types.PrettyPrint
@@ -174,10 +175,12 @@ data SESearch a = Found a | Alts [Symbol]
 
 -- | Functions for Indexed Bind Environment
 
+instance Semigroup IBindEnv where
+  (FB e1) <> (FB e2) = FB (e1 <> e2)
 
 instance Monoid IBindEnv where
-  mempty                  = emptyIBindEnv
-  mappend (FB e1) (FB e2) = FB (e1 `mappend` e2)
+  mempty  = emptyIBindEnv
+  mappend = (<>)
 
 emptyIBindEnv :: IBindEnv
 emptyIBindEnv = FB S.empty
@@ -271,15 +274,20 @@ instance (Fixpoint a) => Fixpoint (SEnv a) where
 instance Fixpoint (SEnv a) => Show (SEnv a) where
   show = render . toFix
 
+instance Semigroup (SEnv a) where
+  s1 <> s2 = SE $ M.union (seBinds s1) (seBinds s2)
+
 instance Monoid (SEnv a) where
   mempty        = SE M.empty
-  mappend s1 s2 = SE $ M.union (seBinds s1) (seBinds s2)
+
+instance Semigroup BindEnv where
+  (BE 0 _) <> b        = b
+  b        <> (BE 0 _) = b
+  _        <> _        = errorstar "mappend on non-trivial BindEnvs"
 
 instance Monoid BindEnv where
-  mempty = BE 0 M.empty
-  mappend (BE 0 _) b = b
-  mappend b (BE 0 _) = b
-  mappend _ _        = errorstar "mappend on non-trivial BindEnvs"
+  mempty  = BE 0 M.empty
+  mappend = (<>)
 
 envCs :: BindEnv -> IBindEnv -> [(Symbol, SortedReft)]
 envCs be env = [lookupBindEnv i be | i <- elemsIBindEnv env]
@@ -317,9 +325,12 @@ instance Fixpoint Packs where
 instance PPrint Packs where
   pprintTidy _ = toFix
 
+instance Semigroup Packs where
+  m1 <> m2 = Packs $ M.union (packm m1) (packm m2)
+
 instance Monoid Packs where
-  mempty        = Packs mempty
-  mappend m1 m2 = Packs $ M.union (packm m1) (packm m2)
+  mempty  = Packs mempty
+  mappend = (<>)
 
 getPack :: KVar -> Packs -> Maybe Int
 getPack k (Packs m) = M.lookup k m
diff --git a/src/Language/Fixpoint/Types/Errors.hs b/src/Language/Fixpoint/Types/Errors.hs
index c6fbfbe99..e3c247ad1 100644
--- a/src/Language/Fixpoint/Types/Errors.hs
+++ b/src/Language/Fixpoint/Types/Errors.hs
@@ -53,6 +53,7 @@ import           Control.Exception
 import           Data.Serialize                (Serialize (..))
 import           Data.Generics                 (Data)
 import           Data.Typeable
+import           Data.Semigroup                (Semigroup (..))
 import           Control.DeepSeq
 -- import           Data.Hashable
 import qualified Data.Binary                   as B
@@ -60,19 +61,17 @@ import           GHC.Generics                  (Generic)
 import           Language.Fixpoint.Types.PrettyPrint
 import           Language.Fixpoint.Types.Spans
 import           Language.Fixpoint.Misc
-import           Text.PrettyPrint.HughesPJ
+import           Text.PrettyPrint.HughesPJ.Compat
 -- import           Text.Printf
 import           Data.Function (on)
 
 -- import           Debug.Trace
 
-#if MIN_VERSION_pretty(1,1,3)
 import qualified Text.PrettyPrint.Annotated.HughesPJ as Ann
 
 deriving instance Generic (Ann.AnnotDetails a)
 instance Serialize a => Serialize (Ann.AnnotDetails a)
 instance Serialize a => Serialize (Ann.Doc a)
-#endif
 
 instance Serialize Error1
 -- FIXME: orphans are bad...
@@ -100,7 +99,7 @@ instance Ord Error1 where
   compare = compare `on` errLoc
 
 instance PPrint Error1 where
-  pprintTidy k (Error1 l msg) = (pprintTidy k l <> ": Error")
+  pprintTidy k (Error1 l msg) = (pprintTidy k l <-> ": Error")
                                 $+$ nest 2 msg
 
 instance PPrint Error where
@@ -172,13 +171,16 @@ instance Eq a => Eq (FixResult a) where
   Safe      == Safe               = True
   _         == _                  = False
 
+instance Semigroup (FixResult a) where
+  Safe        <> x           = x
+  x           <> Safe        = x
+  _           <> c@(Crash{}) = c
+  c@(Crash{}) <> _           = c
+  (Unsafe xs) <> (Unsafe ys) = Unsafe (xs ++ ys)
+
 instance Monoid (FixResult a) where
-  mempty                          = Safe
-  mappend Safe x                  = x
-  mappend x Safe                  = x
-  mappend _ c@(Crash _ _)         = c
-  mappend c@(Crash _ _) _         = c
-  mappend (Unsafe xs) (Unsafe ys) = Unsafe (xs ++ ys)
+  mempty  = Safe
+  mappend = (<>)
 
 instance Functor FixResult where
   fmap f (Crash xs msg)   = Crash (f <$> xs) msg
diff --git a/src/Language/Fixpoint/Types/Graduals.hs b/src/Language/Fixpoint/Types/Graduals.hs
index 134756074..acc270b09 100644
--- a/src/Language/Fixpoint/Types/Graduals.hs
+++ b/src/Language/Fixpoint/Types/Graduals.hs
@@ -43,15 +43,18 @@ import qualified Data.List                 as L
 
 import Control.Monad.State.Lazy
 import Data.Maybe (fromMaybe)
+import Data.Semigroup (Semigroup (..))
 import qualified Language.Fixpoint.SortCheck       as So
 import Language.Fixpoint.Solver.Sanitize (symbolEnv)
 
 
 data GSol = GSol !SymEnv !(M.HashMap KVar (Expr, GradInfo))
 
+instance Semigroup GSol where
+  (GSol e1 m1) <> (GSol e2 m2) = GSol (e1 <> e2) (m1 <> m2)
+
 instance Monoid GSol where
   mempty = GSol mempty mempty
-  mappend (GSol e1 m1) (GSol e2 m2) = GSol (mappend e1 e2) (mappend m1 m2)
 
 instance Show GSol where
   show (GSol _ m) = "GSOL = \n" ++ unlines ((\(k,(e, i)) -> showpp k ++ showInfo i ++  " |-> " ++ showpp (tx e)) <$> M.toList m)
diff --git a/src/Language/Fixpoint/Types/Names.hs b/src/Language/Fixpoint/Types/Names.hs
index 051f909fb..1a36cf74c 100644
--- a/src/Language/Fixpoint/Types/Names.hs
+++ b/src/Language/Fixpoint/Types/Names.hs
@@ -103,6 +103,7 @@ module Language.Fixpoint.Types.Names (
   , bvOrName
   , propConName
   -- HKT , tyAppName
+  , isPrim
   , prims
   , mulFuncName
   , divFuncName
@@ -169,7 +170,9 @@ instance Eq Symbol where
   S i _ _ == S j _ _ = i == j
 
 instance Ord Symbol where
-  compare (S i _ _) (S j _ _) = compare i j
+  -- compare (S i _ _) (S j _ _) = compare i j
+  -- compare s1 s2 = compare (symbolString s1) (symbolString s2)
+  compare s1 s2 = compare (symbolText s1) (symbolText s2)
 
 instance Interned Symbol where
   type Uninterned Symbol = T.Text
@@ -594,40 +597,44 @@ mulFuncName, divFuncName :: Symbol
 mulFuncName  = "Z3_OP_MUL"
 divFuncName  = "Z3_OP_DIV"
 
-prims :: [Symbol]
-prims = [ propConName
-        , _hpropConName
-        , vvName
-        , "Pred"
-        , "List"
-        , "[]"
-        , "bool"
-        -- , "int"
-        -- , "real"
-        , setConName
-        , charConName
-        , "Set_sng"
-        , "Set_cup"
-        , "Set_cap"
-        , "Set_dif"
-        , "Set_emp"
-        , "Set_empty"
-        , "Set_mem"
-        , "Set_sub"
-        , mapConName
-        , "Map_select"
-        , "Map_store"
-        , "Map_union"
-        , "Map_default"
-        , size32Name
-        , size64Name
-        , bitVecName
-        , bvOrName
-        , bvAndName
-        , "FAppTy"
-        , nilName
-        , consName
-        ]
+isPrim :: Symbol -> Bool 
+isPrim x = S.member x prims 
+
+prims :: S.HashSet Symbol
+prims = S.fromList 
+  [ propConName
+  , _hpropConName
+  , vvName
+  , "Pred"
+  , "List"
+  , "[]"
+  , "bool"
+  -- , "int"
+  -- , "real"
+  , setConName
+  , charConName
+  , "Set_sng"
+  , "Set_cup"
+  , "Set_cap"
+  , "Set_dif"
+  , "Set_emp"
+  , "Set_empty"
+  , "Set_mem"
+  , "Set_sub"
+  , mapConName
+  , "Map_select"
+  , "Map_store"
+  , "Map_union"
+  , "Map_default"
+  , size32Name
+  , size64Name
+  , bitVecName
+  , bvOrName
+  , bvAndName
+  , "FAppTy"
+  , nilName
+  , consName
+  ]
 
 {-
 -------------------------------------------------------------------------------
diff --git a/src/Language/Fixpoint/Types/PrettyPrint.hs b/src/Language/Fixpoint/Types/PrettyPrint.hs
index 45b26368b..e03cae833 100644
--- a/src/Language/Fixpoint/Types/PrettyPrint.hs
+++ b/src/Language/Fixpoint/Types/PrettyPrint.hs
@@ -6,16 +6,16 @@
 module Language.Fixpoint.Types.PrettyPrint where
 
 import           Debug.Trace               (trace)
-import           Text.PrettyPrint.HughesPJ
+import           Text.PrettyPrint.HughesPJ.Compat
 import qualified Text.PrettyPrint.Boxes as B
 import qualified Data.HashMap.Strict as M
 import qualified Data.HashSet        as S
 import qualified Data.List           as L
 import           Language.Fixpoint.Misc
 import           Data.Hashable
+import           Data.Semigroup (Semigroup (..))
 import qualified Data.Text as T
 
-
 traceFix     ::  (Fixpoint a) => String -> a -> a
 traceFix s x = trace ("\nTrace: [" ++ s ++ "] : " ++ showFix x) x
 
@@ -97,6 +97,10 @@ notracepp _ x = x
 instance PPrint Doc where
   pprintTidy _ = id
 
+instance (PPrint a, PPrint b) => PPrint (Either a b) where 
+  pprintTidy k (Left  a) = "Left"  <+> pprintTidy k a
+  pprintTidy k (Right b) = "Right" <+> pprintTidy k b
+
 instance PPrint a => PPrint (Maybe a) where
   pprintTidy k = maybe "Nothing" (("Just" <+>) . pprintTidy k)
 
@@ -115,23 +119,23 @@ pprintKVs t = vcat . punctuate "\n" . map pp1
     pp1 (x,y) = pprintTidy t x <+> ":=" <+> pprintTidy t y
 
 instance (PPrint a, PPrint b, PPrint c) => PPrint (a, b, c) where
-  pprintTidy k (x, y, z)  = parens $ pprintTidy k x <> "," <+>
-                                     pprintTidy k y <> "," <+>
+  pprintTidy k (x, y, z)  = parens $ pprintTidy k x <-> "," <+>
+                                     pprintTidy k y <-> "," <+>
                                      pprintTidy k z
 
 
 
 instance (PPrint a, PPrint b, PPrint c, PPrint d) => PPrint (a, b, c, d) where
-  pprintTidy k (w, x, y, z)  = parens $ pprintTidy k w <> "," <+>
-                                        pprintTidy k x <> "," <+>
-                                        pprintTidy k y <> "," <+>
+  pprintTidy k (w, x, y, z)  = parens $ pprintTidy k w <-> "," <+>
+                                        pprintTidy k x <-> "," <+>
+                                        pprintTidy k y <-> "," <+>
                                         pprintTidy k z
 
 instance (PPrint a, PPrint b, PPrint c, PPrint d, PPrint e) => PPrint (a, b, c, d, e) where
-  pprintTidy k (v, w, x, y, z)  = parens $ pprintTidy k v <> "," <+>
-                                           pprintTidy k w <> "," <+>
-                                           pprintTidy k x <> "," <+>
-                                           pprintTidy k y <> "," <+>
+  pprintTidy k (v, w, x, y, z)  = parens $ pprintTidy k v <-> "," <+>
+                                           pprintTidy k w <-> "," <+>
+                                           pprintTidy k x <-> "," <+>
+                                           pprintTidy k y <-> "," <+>
                                            pprintTidy k z
 
 
@@ -164,9 +168,12 @@ instance PPrint T.Text where
 
 newtype DocTable = DocTable [(Doc, Doc)]
 
+instance Semigroup DocTable where
+  DocTable t1 <> DocTable t2 = DocTable (t1 ++ t2)
+
 instance Monoid DocTable where
-  mempty                              = DocTable []
-  mappend (DocTable t1) (DocTable t2) = DocTable (t1 ++ t2)
+  mempty  = DocTable []
+  mappend = (<>)
 
 class PTable a where
   ptable :: a -> DocTable
diff --git a/src/Language/Fixpoint/Types/Refinements.hs b/src/Language/Fixpoint/Types/Refinements.hs
index bc41333f5..32fa52792 100644
--- a/src/Language/Fixpoint/Types/Refinements.hs
+++ b/src/Language/Fixpoint/Types/Refinements.hs
@@ -95,6 +95,7 @@ module Language.Fixpoint.Types.Refinements (
 
   ) where
 
+import           Prelude hiding ((<>))
 import qualified Data.Binary as B
 import           Data.Generics             (Data)
 import           Data.Typeable             (Typeable)
@@ -112,7 +113,7 @@ import           Language.Fixpoint.Types.PrettyPrint
 import           Language.Fixpoint.Types.Spans
 import           Language.Fixpoint.Types.Sorts
 import           Language.Fixpoint.Misc
-import           Text.PrettyPrint.HughesPJ
+import           Text.PrettyPrint.HughesPJ.Compat
 
 -- import           Text.Printf               (printf)
 
@@ -224,7 +225,7 @@ instance Show Subst where
 instance Fixpoint Subst where
   toFix (Su m) = case hashMapToAscList m of
                    []  -> empty
-                   xys -> hcat $ map (\(x,y) -> brackets $ toFix x <> text ":=" <> toFix y) xys
+                   xys -> hcat $ map (\(x,y) -> brackets $ toFix x <-> text ":=" <-> toFix y) xys
 
 instance PPrint Subst where
   pprintTidy _ = toFix
@@ -359,7 +360,7 @@ elit l s = ECon $ L (symbolText $ val l) s
 instance Fixpoint Constant where
   toFix (I i)   = toFix i
   toFix (R i)   = toFix i
-  toFix (L s t) = parens $ text "lit" <+> text "\"" <> toFix s <> text "\"" <+> toFix t
+  toFix (L s t) = parens $ text "lit" <+> text "\"" <-> toFix s <-> text "\"" <+> toFix t
 
 --------------------------------------------------------------------------------
 -- | String Constants ----------------------------------------------------------
@@ -381,7 +382,7 @@ instance Fixpoint SymConst where
   toFix  = toFix . encodeSymConst
 
 instance Fixpoint KVar where
-  toFix (KV k) = text "$" <> toFix k
+  toFix (KV k) = text "$" <-> toFix k
 
 instance Fixpoint Brel where
   toFix Eq  = text "="
@@ -422,7 +423,7 @@ instance Fixpoint Expr where
   toFix (PAnd ps)      = text "&&" <+> toFix ps
   toFix (POr  ps)      = text "||" <+> toFix ps
   toFix (PAtom r e1 e2)  = parens $ toFix e1 <+> toFix r <+> toFix e2
-  toFix (PKVar k su)     = toFix k <> toFix su
+  toFix (PKVar k su)     = toFix k <-> toFix su
   toFix (PAll xts p)     = "forall" <+> (toFix xts
                                         $+$ ("." <+> toFix p))
   toFix (PExist xts p)   = "exists" <+> (toFix xts
@@ -506,8 +507,11 @@ instance PPrint Bop where
 instance PPrint Sort where
   pprintTidy _ = toFix
 
+instance PPrint a => PPrint (TCEmb a) where 
+  pprintTidy k = pprintTidy k . tceToList 
+
 instance PPrint KVar where
-  pprintTidy _ (KV x) = text "$" <> pprint x
+  pprintTidy _ (KV x) = text "$" <-> pprint x
 
 instance PPrint SymConst where
   pprintTidy _ (SL x) = doubleQuotes $ text $ T.unpack x
@@ -551,7 +555,7 @@ instance PPrint Expr where
   pprintPrec _ k (EVar s)        = pprintTidy k s
   -- pprintPrec _ (EBot)          = text "_|_"
   pprintPrec z k (ENeg e)        = parensIf (z > zn) $
-                                   "-" <> pprintPrec (zn + 1) k e
+                                   "-" <-> pprintPrec (zn + 1) k e
     where zn = 2
   pprintPrec z k (EApp f es)     = parensIf (z > za) $
                                    pprintPrec za k f <+> pprintPrec (za+1) k es
@@ -568,8 +572,8 @@ instance PPrint Expr where
     where zi = 1
 
   -- RJ: DO NOT DELETE!
-  pprintPrec _ k (ECst e so)     = parens $ pprint e <+> ":" <+> {- const (text "...") -} (pprintTidy k so)
-  -- pprintPrec z k (ECst e _)      = pprintPrec z k e
+  --  pprintPrec _ k (ECst e so)     = parens $ pprint e <+> ":" <+> {- const (text "...") -} (pprintTidy k so)
+  pprintPrec z k (ECst e _)      = pprintPrec z k e
   pprintPrec _ _ PTrue           = trueD
   pprintPrec _ _ PFalse          = falseD
   pprintPrec z k (PNot p)        = parensIf (z > zn) $
diff --git a/src/Language/Fixpoint/Types/Solutions.hs b/src/Language/Fixpoint/Types/Solutions.hs
index f80e81d39..754b681f4 100644
--- a/src/Language/Fixpoint/Types/Solutions.hs
+++ b/src/Language/Fixpoint/Types/Solutions.hs
@@ -77,6 +77,7 @@ import qualified Data.Maybe                 as Mb
 import qualified Data.HashMap.Strict        as M
 import qualified Data.List                  as L
 import           Data.Generics             (Data)
+import           Data.Semigroup            (Semigroup (..))
 import           Data.Typeable             (Typeable)
 import           Control.Monad (filterM)
 import           Language.Fixpoint.Misc
@@ -90,7 +91,7 @@ import           Language.Fixpoint.Types.Environments
 import           Language.Fixpoint.Types.Constraints
 import           Language.Fixpoint.Types.Substitutions
 import           Language.Fixpoint.SortCheck (elaborate)
-import           Text.PrettyPrint.HughesPJ
+import           Text.PrettyPrint.HughesPJ.Compat
 
 --------------------------------------------------------------------------------
 -- | Update Solution -----------------------------------------------------------
@@ -221,24 +222,26 @@ updateGMap sol gmap = sol {gMap = gmap}
 mapGMap :: Sol b a -> (b -> b) -> Sol b a
 mapGMap sol f = sol {gMap = M.map f (gMap sol)}
 
+instance Semigroup (Sol a b) where
+  s1 <> s2 = Sol { sEnv  = (sEnv s1)  <> (sEnv s2)
+                 , sMap  = (sMap s1)  <> (sMap s2)
+                 , gMap  = (gMap s1)  <> (gMap s2)
+                 , sHyp  = (sHyp s1)  <> (sHyp s2)
+                 , sScp  = (sScp s1)  <> (sScp s2)
+                 , sEbd  = (sEbd s1)  <> (sEbd s2) 
+                 , sxEnv = (sxEnv s1) <> (sxEnv s2) 
+                 }
 
 instance Monoid (Sol a b) where
-  mempty        = Sol { sEnv = mempty 
-                      , sMap = mempty 
-                      , gMap = mempty 
-                      , sHyp = mempty 
-                      , sScp = mempty 
-                      , sEbd = mempty
-                      , sxEnv = mempty
-                      }
-  mappend s1 s2 = Sol { sEnv = mappend (sEnv s1) (sEnv s2)
-                      , sMap = mappend (sMap s1) (sMap s2)
-                      , gMap = mappend (gMap s1) (gMap s2)
-                      , sHyp = mappend (sHyp s1) (sHyp s2)
-                      , sScp = mappend (sScp s1) (sScp s2)
-                      , sEbd = mappend (sEbd s1) (sEbd s2) 
-                      , sxEnv = mappend (sxEnv s1) (sxEnv s2) 
-                      }
+  mempty = Sol { sEnv = mempty 
+               , sMap = mempty 
+               , gMap = mempty 
+               , sHyp = mempty 
+               , sScp = mempty 
+               , sEbd = mempty
+               , sxEnv = mempty
+               }
+  mappend = (<>)
 
 instance Functor (Sol a) where
   fmap f (Sol e s m1 m2 m3 m4 m5) = Sol e (f <$> s) m1 m2 m3 m4 m5
diff --git a/src/Language/Fixpoint/Types/Sorts.hs b/src/Language/Fixpoint/Types/Sorts.hs
index f7726f8e3..37469b439 100644
--- a/src/Language/Fixpoint/Types/Sorts.hs
+++ b/src/Language/Fixpoint/Types/Sorts.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP                        #-}
 {-# LANGUAGE TupleSections              #-}
 {-# LANGUAGE DeriveDataTypeable         #-}
 {-# LANGUAGE DeriveGeneric              #-}
@@ -69,6 +70,7 @@ module Language.Fixpoint.Types.Sorts (
   , tceMember 
   , tceInsert
   , tceInsertWith
+  , tceMap
   ) where
 
 import qualified Data.Binary as B
@@ -76,7 +78,7 @@ import           Data.Generics             (Data)
 import           Data.Typeable             (Typeable)
 import           GHC.Generics              (Generic)
 
-import           Data.Monoid               ()
+import           Data.Semigroup            (Semigroup (..))
 import           Data.Hashable
 import           Data.List                 (foldl')
 import           Control.DeepSeq
@@ -85,10 +87,9 @@ import           Language.Fixpoint.Types.Names
 import           Language.Fixpoint.Types.PrettyPrint
 import           Language.Fixpoint.Types.Spans
 import           Language.Fixpoint.Misc
-import           Text.PrettyPrint.HughesPJ
+import           Text.PrettyPrint.HughesPJ.Compat
 import qualified Data.HashMap.Strict       as M
 
-    
 data FTycon   = TC LocSymbol TCInfo deriving (Ord, Show, Data, Typeable, Generic)
 
 -- instance Show FTycon where
@@ -106,9 +107,12 @@ data TCInfo = TCInfo { tc_isNum :: Bool, tc_isReal :: Bool, tc_isString :: Bool
 mappendFTC :: FTycon -> FTycon -> FTycon
 mappendFTC (TC x i1) (TC _ i2) = TC x (mappend i1 i2)
 
+instance Semigroup TCInfo where
+ TCInfo i1 i2 i3 <> TCInfo i1' i2' i3' = TCInfo (i1 || i1') (i2 || i2') (i3 || i3')
+
 instance Monoid TCInfo where
-  mempty                                          = TCInfo defNumInfo defRealInfo defStrInfo
-  mappend (TCInfo i1 i2 i3)  (TCInfo i1' i2' i3') = TCInfo (i1 || i1') (i2 || i2') (i3 || i3')
+  mempty  = TCInfo defNumInfo defRealInfo defStrInfo
+  mappend = (<>)
 
 defTcInfo, numTcInfo, realTcInfo, strTcInfo :: TCInfo
 defTcInfo  = TCInfo defNumInfo defRealInfo defStrInfo
@@ -342,7 +346,7 @@ instance Fixpoint Sort where
   toFix = toFixSort
 
 toFixSort :: Sort -> Doc
-toFixSort (FVar i)     = text "@" <> parens (toFix i)
+toFixSort (FVar i)     = text "@" <-> parens (toFix i)
 toFixSort FInt         = text "int"
 toFixSort FReal        = text "real"
 toFixSort FFrac        = text "frac"
@@ -354,7 +358,7 @@ toFixSort (FTC c)      = toFix c
 toFixSort t@(FApp _ _) = toFixFApp (unFApp t)
 
 toFixAbsApp :: Sort -> Doc
-toFixAbsApp t = text "func" <> parens (toFix n <> text ", " <> toFix ts)
+toFixAbsApp t = text "func" <-> parens (toFix n <+> text "," <+> toFix ts)
   where
     Just (vs, ss, s) = functionSort t
     n                = length vs
@@ -459,14 +463,16 @@ instance NFData DataCtor
 instance NFData DataDecl
 instance NFData Sub
 
-instance Monoid Sort where
-  mempty            = FObj "any"
-  mappend t1 t2
+instance Semigroup Sort where
+  t1 <> t2
     | t1 == mempty  = t2
     | t2 == mempty  = t1
     | t1 == t2      = t1
     | otherwise     = errorstar $ "mappend-sort: conflicting sorts t1 =" ++ show t1 ++ " t2 = " ++ show t2
 
+instance Monoid Sort where
+  mempty  = FObj "any"
+  mappend = (<>)
 
 -------------------------------------------------------------------------------
 -- | Embedding stuff as Sorts 
@@ -480,12 +486,19 @@ data TCArgs = WithArgs | NoArgs
 tceInsertWith :: (Eq a, Hashable a) => (Sort -> Sort -> Sort) -> a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
 tceInsertWith f k t a (TCE m) = TCE (M.insertWith ff k (t, a) m)
   where 
-    ff (t1, a1) (t2, a2)      = (f t1 t2, mappend a1 a2)
+    ff (t1, a1) (t2, a2)      = (f t1 t2, a1 <> a2)
+
+instance Semigroup TCArgs where 
+  NoArgs <> NoArgs = NoArgs
+  _      <> _      = WithArgs
 
 instance Monoid TCArgs where 
-  mempty                = NoArgs 
-  mappend NoArgs NoArgs = NoArgs
-  mappend _      _      = WithArgs
+  mempty = NoArgs 
+  mappend = (<>)
+
+instance PPrint TCArgs where 
+  pprintTidy _ WithArgs = "*"
+  pprintTidy _ NoArgs   = ""
 
 tceInsert :: (Eq a, Hashable a) => a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
 tceInsert k t a (TCE m) = TCE (M.insert k (t, a) m)
@@ -493,9 +506,16 @@ tceInsert k t a (TCE m) = TCE (M.insert k (t, a) m)
 tceLookup :: (Eq a, Hashable a) => a -> TCEmb a -> Maybe (Sort, TCArgs) 
 tceLookup k (TCE m) = M.lookup k m
 
+instance (Eq a, Hashable a) => Semigroup (TCEmb a) where 
+  (TCE m1) <> (TCE m2) = TCE (m1 <> m2)
+
 instance (Eq a, Hashable a) => Monoid (TCEmb a) where 
-  mempty                    = TCE mempty 
-  mappend (TCE m1) (TCE m2) = TCE (mappend m1 m2)
+  mempty  = TCE mempty 
+  mappend = (<>)
+
+
+tceMap :: (Eq b, Hashable b) => (a -> b) -> TCEmb a -> TCEmb b
+tceMap f = tceFromList . fmap (mapFst f) . tceToList 
 
 tceFromList :: (Eq a, Hashable a) => [(a, (Sort, TCArgs))] -> TCEmb a
 tceFromList = TCE . M.fromList 
@@ -504,4 +524,4 @@ tceToList :: TCEmb a -> [(a, (Sort, TCArgs))]
 tceToList (TCE m) = M.toList m
 
 tceMember :: (Eq a, Hashable a) => a -> TCEmb a -> Bool 
-tceMember k (TCE m) = M.member k m
\ No newline at end of file
+tceMember k (TCE m) = M.member k m
diff --git a/src/Language/Fixpoint/Types/Spans.hs b/src/Language/Fixpoint/Types/Spans.hs
index 9287dd0dd..4c74985e3 100644
--- a/src/Language/Fixpoint/Types/Spans.hs
+++ b/src/Language/Fixpoint/Types/Spans.hs
@@ -25,6 +25,7 @@ module Language.Fixpoint.Types.Spans (
 
   -- * Destructing spans
   , sourcePosElts
+  , srcLine 
   ) where
 
 -- import           Control.Exception
@@ -111,7 +112,6 @@ instance Fixpoint a => Fixpoint (Located a) where
 instance Functor Located where
   fmap f (Loc l l' x) =  Loc l l' (f x)
 
-
 instance Foldable Located where
   foldMap f (Loc _ _ x) = f x
 
@@ -140,6 +140,8 @@ instance Hashable a => Hashable (Located a) where
 instance (IsString a) => IsString (Located a) where
   fromString = dummyLoc . fromString
 
+srcLine :: (Loc a) => a -> Int 
+srcLine = sourceLine . sp_start . srcSpan 
 
 -----------------------------------------------------------------------
 -- | A Reusable SrcSpan Type ------------------------------------------
diff --git a/src/Language/Fixpoint/Types/Substitutions.hs b/src/Language/Fixpoint/Types/Substitutions.hs
index 6ab870a43..7487467d8 100644
--- a/src/Language/Fixpoint/Types/Substitutions.hs
+++ b/src/Language/Fixpoint/Types/Substitutions.hs
@@ -14,17 +14,21 @@ module Language.Fixpoint.Types.Substitutions (
 import           Data.Maybe
 import qualified Data.HashMap.Strict       as M
 import qualified Data.HashSet              as S
+import           Data.Semigroup            (Semigroup (..))
 import           Language.Fixpoint.Types.PrettyPrint
 import           Language.Fixpoint.Types.Names
 import           Language.Fixpoint.Types.Sorts
 import           Language.Fixpoint.Types.Refinements
 import           Language.Fixpoint.Misc
-import           Text.PrettyPrint.HughesPJ
+import           Text.PrettyPrint.HughesPJ.Compat
 import           Text.Printf               (printf)
 
+instance Semigroup Subst where
+  (<>) = catSubst
+
 instance Monoid Subst where
   mempty  = emptySubst
-  mappend = catSubst
+  mappend = (<>)
 
 filterSubst :: (Symbol -> Expr -> Bool) -> Subst -> Subst
 filterSubst f (Su m) = Su (M.filterWithKey f m)
@@ -38,7 +42,6 @@ catSubst (Su s1) θ2@(Su s2) = Su $ M.union s1' s2
     s1'                     = subst θ2 <$> s1
 
 mkSubst :: [(Symbol, Expr)] -> Subst
-
 mkSubst = Su . M.fromList . reverse . filter notTrivial
   where
     notTrivial (x, EVar y) = x /= y
@@ -50,6 +53,8 @@ isEmptySubst (Su xes) = M.null xes
 targetSubstSyms :: Subst -> [Symbol]
 targetSubstSyms (Su ms) = syms $ M.elems ms
 
+
+  
 instance Subable () where
   syms _      = []
   subst _ ()  = ()
@@ -64,10 +69,17 @@ instance (Subable a, Subable b) => Subable (a,b) where
 
 instance Subable a => Subable [a] where
   syms   = concatMap syms
-  subst  = map . subst
-  substf = map . substf
-  substa = map . substa
+  subst  = fmap . subst
+  substf = fmap . substf
+  substa = fmap . substa
+
+instance Subable a => Subable (Maybe a) where
+  syms   = concatMap syms . maybeToList
+  subst  = fmap . subst
+  substf = fmap . substf
+  substa = fmap . substa
 
+ 
 instance Subable a => Subable (M.HashMap k a) where
   syms   = syms . M.elems
   subst  = M.map . subst
@@ -159,14 +171,20 @@ disjoint (Su su) bs = S.null $ suSyms `S.intersection` bsSyms
     suSyms = S.fromList $ syms (M.elems su) ++ syms (M.keys su)
     bsSyms = S.fromList $ syms $ fst <$> bs
 
+instance Semigroup Expr where
+  p <> q = pAnd [p, q]
+
 instance Monoid Expr where
-  mempty      = PTrue
-  mappend p q = pAnd [p, q]
-  mconcat     = pAnd
+  mempty  = PTrue
+  mappend = (<>)
+  mconcat = pAnd
+
+instance Semigroup Reft where
+  (<>) = meetReft
 
 instance Monoid Reft where
   mempty  = trueReft
-  mappend = meetReft
+  mappend = (<>)
 
 meetReft :: Reft -> Reft -> Reft
 meetReft (Reft (v, ra)) (Reft (v', ra'))
@@ -174,9 +192,12 @@ meetReft (Reft (v, ra)) (Reft (v', ra'))
   | v == dummySymbol = Reft (v', ra' `mappend` (ra `subst1`  (v , EVar v')))
   | otherwise        = Reft (v , ra  `mappend` (ra' `subst1` (v', EVar v )))
 
+instance Semigroup SortedReft where
+  t1 <> t2 = RR (mappend (sr_sort t1) (sr_sort t2)) (mappend (sr_reft t1) (sr_reft t2))
+
 instance Monoid SortedReft where
-  mempty        = RR mempty mempty
-  mappend t1 t2 = RR (mappend (sr_sort t1) (sr_sort t2)) (mappend (sr_reft t1) (sr_reft t2))
+  mempty  = RR mempty mempty
+  mappend = (<>)
 
 instance Subable Reft where
   syms (Reft (v, ras))      = v : syms ras
diff --git a/src/Language/Fixpoint/Types/Theories.hs b/src/Language/Fixpoint/Types/Theories.hs
index fe3a60d6a..4cc46c252 100644
--- a/src/Language/Fixpoint/Types/Theories.hs
+++ b/src/Language/Fixpoint/Types/Theories.hs
@@ -32,6 +32,7 @@ module Language.Fixpoint.Types.Theories (
 
 
 import           Data.Generics             (Data)
+import           Data.Semigroup            (Semigroup (..))
 import           Data.Typeable             (Typeable)
 import           Data.Hashable
 import           GHC.Generics              (Generic)
@@ -42,7 +43,7 @@ import           Language.Fixpoint.Types.Sorts
 import           Language.Fixpoint.Types.Errors
 import           Language.Fixpoint.Types.Environments
 
-import           Text.PrettyPrint.HughesPJ
+import           Text.PrettyPrint.HughesPJ.Compat
 import qualified Data.Text.Lazy           as LT
 import qualified Data.Binary              as B
 import qualified Data.HashMap.Strict      as M
@@ -72,14 +73,17 @@ type FuncSort = (SmtSort, SmtSort)
 instance NFData   SymEnv
 instance B.Binary SymEnv
 
+instance Semigroup SymEnv where
+  e1 <> e2 = SymEnv { seSort   = seSort   e1 <> seSort   e2
+                    , seTheory = seTheory e1 <> seTheory e2
+                    , seData   = seData   e1 <> seData   e2
+                    , seLits   = seLits   e1 <> seLits   e2
+                    , seAppls  = seAppls  e1 <> seAppls  e2
+                    }
+
 instance Monoid SymEnv where
   mempty        = SymEnv emptySEnv emptySEnv emptySEnv emptySEnv mempty
-  mappend e1 e2 = SymEnv { seSort   = seSort   e1 `mappend` seSort   e2
-                         , seTheory = seTheory e1 `mappend` seTheory e2
-                         , seData   = seData   e1 `mappend` seData   e2
-                         , seLits   = seLits   e1 `mappend` seLits   e2
-                         , seAppls  = seAppls  e1 `mappend` seAppls  e2
-                         }
+  mappend       = (<>)
 
 symEnv :: SEnv Sort -> SEnv TheorySymbol -> [DataDecl] -> SEnv Sort -> [Sort] -> SymEnv
 symEnv xEnv fEnv ds ls ts = SymEnv xEnv' fEnv dEnv ls sortMap
@@ -272,7 +276,7 @@ instance PPrint SmtSort where
   pprintTidy _ SSet         = text "Set"
   pprintTidy _ SMap         = text "Map"
   pprintTidy _ (SBitVec n)  = text "BitVec" <+> int n
-  pprintTidy _ (SVar i)     = text "@" <> int i
+  pprintTidy _ (SVar i)     = text "@" <-> int i
 --  HKT pprintTidy k (SApp ts)    = ppParens k (pprintTidy k tyAppName) ts
   pprintTidy k (SData c ts) = ppParens k (pprintTidy k c)         ts
 
diff --git a/src/Language/Fixpoint/Types/Visitor.hs b/src/Language/Fixpoint/Types/Visitor.hs
index da24b23e2..a773c8eae 100644
--- a/src/Language/Fixpoint/Types/Visitor.hs
+++ b/src/Language/Fixpoint/Types/Visitor.hs
@@ -50,6 +50,7 @@ module Language.Fixpoint.Types.Visitor (
 
 -- import           Control.Monad.Trans.State.Strict (State, modify, runState)
 -- import           Control.DeepSeq
+import           Data.Semigroup      (Semigroup (..))
 import           Control.Monad.State.Strict
 import qualified Data.HashSet        as S
 import qualified Data.HashMap.Strict as M
@@ -248,9 +249,12 @@ mapKVarSubsts f          = trans kvVis () ()
 
 newtype MInt = MInt Integer -- deriving (Eq, NFData)
 
+instance Semigroup MInt where
+  MInt m <> MInt n = MInt (m + n)
+
 instance Monoid MInt where
-  mempty                    = MInt 0
-  mappend (MInt m) (MInt n) = MInt (m + n)
+  mempty  = MInt 0
+  mappend = (<>)
 
 size :: Visitable t => t -> Integer
 size t    = n
@@ -328,8 +332,7 @@ stripCasts = trans (defaultVisitor { txExpr = const go }) () ()
 --   to the ty-vars that they should be substituted with. Note the
 --   domain and range are both Symbol and not the Int used for real ty-vars.
 --------------------------------------------------------------------------------
-
-type CoSub = M.HashMap Symbol Sort -- Symbol
+type CoSub = M.HashMap Symbol Sort 
 
 applyCoSub :: CoSub -> Expr -> Expr
 applyCoSub coSub      = mapExpr fE
diff --git a/src/Text/PrettyPrint/HughesPJ/Compat.hs b/src/Text/PrettyPrint/HughesPJ/Compat.hs
new file mode 100644
index 000000000..79d8dccb5
--- /dev/null
+++ b/src/Text/PrettyPrint/HughesPJ/Compat.hs
@@ -0,0 +1,13 @@
+module Text.PrettyPrint.HughesPJ.Compat (
+    module Text.PrettyPrint.HughesPJ,
+    (<->),
+    ) where
+
+import Text.PrettyPrint.HughesPJ hiding ((<>), first)
+import qualified Text.PrettyPrint.HughesPJ as PP
+
+-- | Also known as '<>' in @pretty@, but that clashes with Semigroup's <>
+(<->) :: Doc -> Doc -> Doc
+(<->) = (PP.<>)
+
+infixl 6 <->
diff --git a/stack.yaml b/stack.yaml
index e223c3fc4..3cfd57e0a 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,5 +1,4 @@
-
-resolver: lts-8.9
+resolver: lts-12.2
 
 flags:
   liquid-fixpoint:
@@ -7,10 +6,14 @@ flags:
 
 packages:
 - '.'
+
+packages:
+- '.'
+
 extra-deps:
 - dotgen-0.4.2
 - fgl-visualize-0.1.0.1
-- intern-0.9.1.4
-- located-base-0.1.1.0
-
-# resolver: nightly-2016-05-21
+- intern-0.9.2
+- located-base-0.1.1.1
+- tasty-rerun-1.1.12
+- text-format-0.3.2