diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -2,6 +2,10 @@
 
 ## NEXT
 
+## 0.9.6.3 (2024-01-29)
+
+- For now we stopped folding constants that contain NaN [#670](https://github.com/ucsd-progsys/liquid-fixpoint/pull/670)
+
 ## 0.9.4.7
 
 - Support GHC 9.6 tuples with `--extensionality` [#666](https://github.com/ucsd-progsys/liquid-fixpoint/issues/641) [#667](https://github.com/ucsd-progsys/liquid-fixpoint/issues/641)
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.4.7
+version:            0.9.6.3
 synopsis:           Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
 description:
   This package implements an SMTLIB based Horn-Clause\/Logical Implication constraint
diff --git a/src/Language/Fixpoint/Defunctionalize.hs b/src/Language/Fixpoint/Defunctionalize.hs
--- a/src/Language/Fixpoint/Defunctionalize.hs
+++ b/src/Language/Fixpoint/Defunctionalize.hs
@@ -3,8 +3,6 @@
 {-# LANGUAGE TupleSections        #-}
 {-# LANGUAGE OverloadedStrings    #-}
 
-{-# OPTIONS_GHC -Wno-name-shadowing #-}
-
 --------------------------------------------------------------------------------
 -- | `defunctionalize` traverses the query to:
 --      1. "normalize" lambda terms by renaming binders,
diff --git a/src/Language/Fixpoint/Horn/Solve.hs b/src/Language/Fixpoint/Horn/Solve.hs
--- a/src/Language/Fixpoint/Horn/Solve.hs
+++ b/src/Language/Fixpoint/Horn/Solve.hs
@@ -1,5 +1,3 @@
-{-# OPTIONS_GHC -Wno-name-shadowing #-}
-
 -------------------------------------------------------------------------------
 -- | This module defines a function to solve NNF constraints,
 --   by reducing them to the standard FInfo.
@@ -29,20 +27,20 @@
 ----------------------------------------------------------------------------------
 solveHorn :: F.Config -> IO ExitCode
 ----------------------------------------------------------------------------------
-solveHorn cfg = do
-  (q, opts) <- parseQuery cfg
+solveHorn baseCfg = do
+  (q, opts) <- parseQuery baseCfg
 
   -- If you want to set --eliminate=none, you better make it a pragma
-  cfg <- if F.eliminate cfg == F.None
-           then pure (cfg { F.eliminate =  F.Some })
-           else pure cfg
+  cfgElim <- if F.eliminate baseCfg == F.None
+           then pure (baseCfg { F.eliminate =  F.Some })
+           else pure baseCfg
 
-  cfg <- F.withPragmas cfg opts
+  cfgPragmas <- F.withPragmas cfgElim opts
 
-  when (F.save cfg) (saveHornQuery cfg q)
+  when (F.save cfgPragmas) (saveHornQuery cfgPragmas q)
 
-  r <- solve cfg q
-  Solver.resultExitCode cfg r
+  r <- solve cfgPragmas q
+  Solver.resultExitCode cfgPragmas r
 
 parseQuery :: F.Config -> IO (H.Query H.Tag, [String])
 parseQuery cfg
@@ -73,9 +71,9 @@
 solve :: (F.PPrint a, NFData a, F.Loc a, Show a, F.Fixpoint a) => F.Config -> H.Query a
        -> IO (F.Result (Integer, a))
 ----------------------------------------------------------------------------------
-solve cfg q = do
-  let c = Tx.uniq $ Tx.flatten $ H.qCstr q
+solve cfg qry = do
+  let c = Tx.uniq $ Tx.flatten $ H.qCstr qry
   whenLoud $ putStrLn "Horn Uniq:"
   whenLoud $ putStrLn $ F.showpp c
-  q <- eliminate cfg ({- void $ -} q { H.qCstr = c })
+  q <- eliminate cfg ({- void $ -} qry { H.qCstr = c })
   Solver.solve cfg (hornFInfo cfg q)
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
@@ -4,7 +4,6 @@
 {-# LANGUAGE FlexibleInstances  #-}
 
 {-# OPTIONS_GHC -Wno-orphans        #-}
-{-# OPTIONS_GHC -Wno-name-shadowing #-}
 
 module Language.Fixpoint.Horn.Transformations (
     uniq
@@ -53,8 +52,8 @@
                M.HashMap a1 ((a4, a2), a3) -> IO ()
 printPiSols piSols =
   mapM_
-    (\(piVar, ((_, args), cstr)) -> do
-                  putStr $ F.showpp piVar
+    (\(piVar', ((_, args), cstr)) -> do
+                  putStr $ F.showpp piVar'
                   putStr " := "
                   putStrLn $ F.showpp args
                   putStrLn $ F.showpp cstr
@@ -74,14 +73,14 @@
 
 solveEbs :: (F.PPrint a) => F.Config -> Query a -> IO (Query a)
 ------------------------------------------------------------------------------
-solveEbs cfg query@(Query qs vs c cons dist eqns mats dds) = do
+solveEbs cfg query@(Query qs vs cstr cons dist eqns mats dds) = do
   -- clean up
-  let normalizedC = flatten . pruneTauts $ hornify c
+  let normalizedC = flatten . pruneTauts $ hornify cstr
   whenLoud $ putStrLn "Normalized EHC:"
   whenLoud $ putStrLn $ F.showpp normalizedC
 
   -- short circuit if no ebinds are present
-  if isNNF c then pure $ Query qs vs normalizedC cons dist eqns mats dds else do
+  if isNNF cstr then pure $ Query qs vs normalizedC cons dist eqns mats dds else do
   let kvars = boundKvars normalizedC
 
   whenLoud $ putStrLn "Skolemized:"
@@ -105,17 +104,17 @@
   let acyclicKs = kvars `S.difference` cuts
 
   whenLoud $ putStrLn "solved acyclic kvars:"
-  let (horn', side') = elimKs' (S.toList acyclicKs) (horn, side)
-  whenLoud $ putStrLn $ F.showpp horn'
-  whenLoud $ putStrLn $ F.showpp side'
+  let (hornk, sidek) = elimKs' (S.toList acyclicKs) (horn, side)
+  whenLoud $ putStrLn $ F.showpp hornk
+  whenLoud $ putStrLn $ F.showpp sidek
 
   -- if not $ S.null cuts then error $ F.showpp $ S.toList cuts else pure ()
   let elimCutK k c = doelim k [] c
-  horn' <- pure $ foldr elimCutK horn' cuts
-  side' <- pure $ foldr elimCutK side' cuts
+      hornCut = foldr elimCutK hornk cuts
+      sideCut = foldr elimCutK sidek cuts
 
   whenLoud $ putStrLn "pi defining constraints:"
-  let piSols = M.fromList $ fmap (\pivar -> (pivar, piDefConstr pivar horn')) (S.toList pivars)
+  let piSols = M.fromList $ fmap (\pivar -> (pivar, piDefConstr pivar hornCut)) (S.toList pivars)
   whenLoud $ printPiSols piSols
 
   whenLoud $ putStrLn "solved pis:"
@@ -123,11 +122,11 @@
   whenLoud $ putStrLn $ F.showpp solvedPiCstrs
 
   whenLoud $ putStrLn "solved horn:"
-  let solvedHorn = substPiSols solvedPiCstrs horn'
+  let solvedHorn = substPiSols solvedPiCstrs hornCut
   whenLoud $ putStrLn $ F.showpp solvedHorn
 
   whenLoud $ putStrLn "solved side:"
-  let solvedSide = substPiSols solvedPiCstrs side'
+  let solvedSide = substPiSols solvedPiCstrs sideCut
   whenLoud $ putStrLn $ F.showpp solvedSide
 
   pure (Query qs vs (CAnd [solvedHorn, solvedSide]) cons dist eqns mats dds)
@@ -135,14 +134,14 @@
 -- | Collects the defining constraint for π
 -- that is, given `∀ Γ.∀ n.π => c`, returns `((π, n:Γ), c)`
 piDefConstr :: F.Symbol -> Cstr a -> ((F.Symbol, [F.Symbol]), Cstr a)
-piDefConstr k c = ((head ns, head formals), defC)
+piDefConstr k c = ((head syms, head formalSyms), defCStr)
   where
-    (ns, formals, defC) = case go c of
+    (syms, formalSyms, defCStr) = case go c of
       (ns, formals, Just defC) -> (ns, formals, defC)
       (_, _, Nothing) -> error $ "pi variable " <> F.showpp k <> " has no defining constraint."
 
     go :: Cstr a -> ([F.Symbol], [[F.Symbol]], Maybe (Cstr a))
-    go (CAnd cs) = (\(as, bs, cs) -> (concat as, concat bs, cAndMaybes cs)) $ unzip3 $ go <$> cs
+    go (CAnd cs) = (\(as, bs, mcs) -> (concat as, concat bs, cAndMaybes mcs)) $ unzip3 $ go <$> cs
     go (All b@(Bind n _ (Var k' xs) _) c')
       | k == k' = ([n], [S.toList $ S.fromList xs `S.difference` S.singleton n], Just c')
       | otherwise = map3 (fmap (All b)) (go c')
@@ -159,18 +158,18 @@
 
 -- | Solve out the given pivars
 solPis :: S.Set F.Symbol -> M.HashMap F.Symbol ((F.Symbol, [F.Symbol]), Cstr a) -> M.HashMap F.Symbol Pred
-solPis measures piSols = go (M.toList piSols) piSols
+solPis measures piSolsMap = go (M.toList piSolsMap) piSolsMap
   where
-    go ((pi, ((n, xs), c)):pis) piSols = M.insert pi solved $ go pis piSols
-      where solved = solPi measures pi n (S.fromList xs) piSols c
+    go ((pi', ((n, xs), c)):pis) piSols = M.insert pi' solved $ go pis piSols
+      where solved = solPi measures pi' n (S.fromList xs) piSols c
     go [] _ = mempty
 
 -- TODO: rewrite to use CC
 solPi :: S.Set F.Symbol -> F.Symbol -> F.Symbol -> S.Set F.Symbol -> M.HashMap F.Symbol ((F.Symbol, [F.Symbol]), Cstr a) -> Cstr a -> Pred
-solPi measures basePi n args piSols c = trace ("\n\nsolPi: " <> F.showpp basePi <> "\n\n" <> F.showpp n <> "\n" <> F.showpp (S.toList args) <> "\n" <> F.showpp ((\(a, _, c) -> (a, c)) <$> edges) <> "\n" <> F.showpp (sols n) <> "\n" <> F.showpp rewritten <> "\n" <> F.showpp c <> "\n\n") $ PAnd rewritten
+solPi measures basePi n args piSols cstr = trace ("\n\nsolPi: " <> F.showpp basePi <> "\n\n" <> F.showpp n <> "\n" <> F.showpp (S.toList args) <> "\n" <> F.showpp ((\(a, _, c) -> (a, c)) <$> edges) <> "\n" <> F.showpp (sols n) <> "\n" <> F.showpp rewritten <> "\n" <> F.showpp cstr <> "\n\n") $ PAnd rewritten
   where
     rewritten = rewriteWithEqualities measures n args equalities
-    equalities = (nub . fst) $ go (S.singleton basePi) c
+    equalities = (nub . fst) $ go (S.singleton basePi) cstr
     edges = eqEdges args mempty equalities
     (eGraph, vf, lookupVertex) = DG.graphFromEdges edges
     sols x = case lookupVertex x of
@@ -178,12 +177,12 @@
       Just vertex -> nub $ filter (/= F.EVar x) $ mconcat [es | ((_, es), _, _) <- vf <$> DG.reachable eGraph vertex]
 
     go :: S.Set F.Symbol -> Cstr a -> ([(F.Symbol, F.Expr)], S.Set F.Symbol)
-    go visited (Head p _) = (collectEqualities p, visited)
-    go visited (CAnd cs) = foldl' (\(eqs, visited) c -> let (eqs', visited') = go visited c in (eqs' <> eqs, visited')) (mempty, visited) cs
-    go visited (All (Bind _ _ (Var pi _) _) c)
-      | S.member pi visited = go visited c
-      | otherwise = let (_, defC) = (piSols M.! pi)
-                        (eqs', newVisited) = go (S.insert pi visited) defC
+    go visitedSyms (Head p _) = (collectEqualities p, visitedSyms)
+    go visitedSyms (CAnd cs) = foldl' (\(eqs, visited) c -> let (eqs', visited') = go visited c in (eqs' <> eqs, visited')) (mempty, visitedSyms) cs
+    go visited (All (Bind _ _ (Var pi' _) _) c)
+      | S.member pi' visited = go visited c
+      | otherwise = let (_, defC) = (piSols M.! pi')
+                        (eqs', newVisited) = go (S.insert pi' visited) defC
                         (eqs'', newVisited') = go newVisited c in
           (eqs' <> eqs'', newVisited')
     go visited (All (Bind _ _ p _) c) = let (eqs, visited') = go visited c in
@@ -242,11 +241,11 @@
     go _ (Head c l) = Head c l
     go xs (CAnd c)   = CAnd (go xs <$> c)
     go xs (All b c2) = All b $ go (bSym b : xs) c2
-    go xs (Any b@(Bind x t p ann) c2) = CAnd [All b' $ CAnd [Head p l, go (x:xs) c2], Any b (Head pi l)]
+    go xs (Any b@(Bind x t p ann) c2) = CAnd [All b' $ CAnd [Head p l, go (x:xs) c2], Any b (Head pi' l)]
       -- TODO: actually use the renamer?
       where
-        b' = Bind x t pi ann
-        pi = piVar x xs
+        b' = Bind x t pi' ann
+        pi' = piVar x xs
         l  = cLabel c2
 
 piVar :: F.Symbol -> [F.Symbol] -> Pred
@@ -330,7 +329,7 @@
 split c@Head{} = (Just c, Nothing)
 
 andMaybes :: [Maybe (Cstr a)] -> Maybe (Cstr a)
-andMaybes cs = case catMaybes cs of
+andMaybes mcs = case catMaybes mcs of
                  [] -> Nothing
                  [c] -> Just c
                  cs -> Just $ CAnd cs
@@ -386,31 +385,31 @@
 elimPis [] cc = cc
 elimPis (n:ns) (horn, side) = elimPis ns (apply horn, apply side)
 -- TODO: handle this error?
-  where nSol = case defs n horn of
+  where nSol' = case defs n horn of
                  Just nSol -> nSol
                  Nothing -> error "Unexpected nothing elimPis"
 
-        apply = applyPi (piSym n) nSol
+        apply = applyPi (piSym n) nSol'
 
 -- TODO: PAnd may be a problem
 applyPi :: F.Symbol -> Cstr a -> Cstr a -> Cstr a
-applyPi k defs (All (Bind x t (Var k' _xs) ann) c)
+applyPi k defCstr (All (Bind x t (Var k' _xs) ann) c)
   | k == k'
-  = All (Bind x t (Reft $ cstrToExpr defs) ann) c
+  = All (Bind x t (Reft $ cstrToExpr defCstr) ann) c
 applyPi k bp (CAnd cs)
   = CAnd $ applyPi k bp <$> cs
 applyPi k bp (All b c)
   = All b (applyPi k bp c)
 applyPi k bp (Any b c)
   = Any b (applyPi k bp c)
-applyPi k defs (Head (Var k' _xs) a)
+applyPi k defCstr (Head (Var k' _xs) a)
   | k == k'
   -- what happens when pi's appear inside the defs for other pis?
   -- this shouldn't happen because there should be a strict
   --  pi -> k -> pi structure
   -- but that comes from the typing rules, not this format, so let's make
   -- it an invariant of solveEbs above
-  = Head (Reft $ cstrToExpr defs) a
+  = Head (Reft $ cstrToExpr defCstr) a
 applyPi _ _ (Head p a) = Head p a
 
 -- | The defining constraints for a pivar
@@ -647,15 +646,15 @@
     isWellFormed e = S.fromList (F.syms e) `S.isSubsetOf` argsAndPrims
 
     makeWellFormed :: Int -> [F.Expr] -> [F.Expr]
-    makeWellFormed 0 es = filter isWellFormed es -- We solved it. Maybe.
-    makeWellFormed n es = makeWellFormed (n - 1) $ mconcat $ go <$> es
+    makeWellFormed 0 exprs = filter isWellFormed exprs -- We solved it. Maybe.
+    makeWellFormed m exprs = makeWellFormed (m - 1) $ mconcat $ go <$> exprs
       where
-        go e = if isWellFormed e then [e] else rewrite rewrites [e]
+        go expr = if isWellFormed expr then [expr] else rewrite rewrites [expr]
           where
-            needSolving = S.fromList (F.syms e) `S.difference` argsAndPrims
+            needSolving = S.fromList (F.syms expr) `S.difference` argsAndPrims
             rewrites = (\x -> (x, filter (/= F.EVar x) $ sols x)) <$> S.toList needSolving
             rewrite [] es = es
-            rewrite ((x, rewrites):rewrites') es = rewrite rewrites' $ [F.subst (F.mkSubst [(x, e')]) e | e' <- rewrites, e <- es]
+            rewrite ((x, rewriteExprs):rewriteExprs') es = rewrite rewriteExprs' $ [F.subst (F.mkSubst [(x, e')]) e | e' <- rewriteExprs, e <- es]
 
 eqEdges :: S.Set F.Symbol ->
            M.HashMap F.Symbol ([F.Symbol], [F.Expr]) ->
@@ -694,14 +693,14 @@
   | Var k _ <- p = All (Bind x t (M.lookupDefault p k piSols) l) (substPiSols piSols c)
   | otherwise = All (Bind x t p l) (substPiSols piSols c)
 substPiSols piSols (Any (Bind n _ p _) c)
-  | Head (Var pi _) label <- c, Just sol <- M.lookup pi piSols =
+  | Head (Var pi' _) label <- c, Just sol <- M.lookup pi' piSols =
     case findSol n sol of
-      Just e -> Head (flatten $ PAnd $ (\pred -> F.subst1 pred (n, e)) <$> [p, sol]) label
+      Just e -> Head (flatten $ PAnd $ (\predFn -> F.subst1 predFn (n, e)) <$> [p, sol]) label
       Nothing -> Head (Reft $ F.PAnd []) label
   | otherwise = error "missing piSol"
 
 findSol :: F.Symbol -> Pred -> Maybe F.Expr
-findSol x = go
+findSol sym = go
   where
     go (Reft e) = findEq e
     go Var{} = Nothing
@@ -710,8 +709,8 @@
       x:_ -> Just x
 
     findEq (F.PAtom F.Eq left right)
-      | F.EVar y <- left, y == x = Just right
-      | F.EVar y <- right, y == x = Just left
+      | F.EVar y <- left, y == sym = Just right
+      | F.EVar y <- right, y == sym = Just left
     findEq _ = Nothing
 
 ------------------------------------------------------------------------------
@@ -812,10 +811,10 @@
     -- if kvar doesn't appear, then just return the left
     -- if kvar appears in one child, that is the lca
     -- but if kvar appear in multiple chlidren, this is the lca
-    go c@(CAnd cs) = case rights (go <$> cs) of
-                       [] -> Left $ cLabel c
+    go cstr'@(CAnd cs) = case rights (go <$> cs) of
+                       [] -> Left $ cLabel cstr'
                        [c] -> Right c
-                       _ -> Right c
+                       _ -> Right cstr'
 
 
 -- | A solution is a Hyp of binders (including one anonymous binder
@@ -857,20 +856,20 @@
 -- (forall ((v bool) (v)) (forall ((z int) (donkey)) ((z == x))))
 
 doelim :: F.Symbol -> [([Bind a], [F.Expr])] -> Cstr a -> Cstr a
-doelim k bss (CAnd cs)
-  = CAnd $ doelim k bss <$> cs
-doelim k bss (All (Bind x t p l) c) =
-  case findKVarInGuard k p of
-    Right _ -> All (Bind x t p l) (doelim k bss c)
-    Left (kvars, preds) -> demorgan x t l kvars preds (doelim k bss c) bss
+doelim sym bss (CAnd cs)
+  = CAnd $ doelim sym bss <$> cs
+doelim sym bss (All (Bind sym' sort' p l) cstr) =
+  case findKVarInGuard sym p of
+    Right _ -> All (Bind sym' sort' p l) (doelim sym bss cstr)
+    Left (kvars, preds) -> demorgan sym' sort' l kvars preds (doelim sym bss cstr) bss
   where
     demorgan :: F.Symbol -> F.Sort -> a -> [(F.Symbol, [F.Symbol])] -> [Pred] -> Cstr a -> [([Bind a], [F.Expr])] -> Cstr a
-    demorgan x t ann kvars preds c bss = mkAnd $ cubeSol <$> bss
+    demorgan x t ann kvars preds cstr' bindExprs = mkAnd $ cubeSol <$> bindExprs
       where su = F.Su $ M.fromList $ concatMap (\(k, xs) -> zip (kargs k) (F.EVar <$> xs)) kvars
             mkAnd [c] = c
             mkAnd cs = CAnd cs
             cubeSol (b:bs, eqs) = All b $ cubeSol (bs, eqs)
-            cubeSol ([], eqs) = All (Bind x t (PAnd $ (Reft <$> F.subst su eqs) ++ (F.subst su <$> preds)) ann) c
+            cubeSol ([], eqs) = All (Bind x t (PAnd $ (Reft <$> F.subst su eqs) ++ (F.subst su <$> preds)) ann) cstr'
 doelim k _ (Head (Var k' _) a)
   | k == k'
   = Head (Reft F.PTrue) a
@@ -879,7 +878,7 @@
 doelim k bss (Any (Bind x t p l) c) =
   case findKVarInGuard k p of
     Right _ -> Any (Bind x t p l) (doelim k bss c)
-    Left (_, rights) -> Any (Bind x t (PAnd rights) l) (doelim k bss c) -- TODO: for now we set the kvar to true. not sure if this is correct
+    Left (_, rights') -> Any (Bind x t (PAnd rights') l) (doelim k bss c) -- TODO: for now we set the kvar to true. not sure if this is correct
 
 -- If k is in the guard then returns a Left list of that k and the remaining preds in the guard
 -- If k is not in the guard returns a Right of the pred
@@ -889,9 +888,9 @@
     then Right (PAnd ps) -- kvar not found
     else Left (newLefts, newRights)
   where findResults = findKVarInGuard k <$> ps
-        (lefts, rights) = partitionEithers findResults
+        (lefts, rights') = partitionEithers findResults
         newLefts = concatMap fst lefts
-        newRights = concatMap snd lefts ++ rights
+        newRights = concatMap snd lefts ++ rights'
 findKVarInGuard k p@(Var k' xs)
   | k == k' = Left ([(k', xs)], [])
   | otherwise = Right p
@@ -970,7 +969,7 @@
   flatten :: a -> a
 
 instance Flatten (Cstr a) where
-  flatten (CAnd cs) = case flatten cs of
+  flatten (CAnd cstrs) = case flatten cstrs of
                         [c] -> c
                         cs -> CAnd cs
   flatten (Head p a) = Head (flatten p) a
@@ -987,7 +986,7 @@
   flatten [] = []
 
 instance Flatten Pred where
-  flatten (PAnd ps) = case flatten ps of
+  flatten (PAnd preds) = case flatten preds of
                         [p] -> p
                         ps  -> PAnd ps
   flatten p = p
@@ -1002,7 +1001,7 @@
   flatten []              = []
 
 instance Flatten F.Expr where
-  flatten (F.PAnd ps) = case flatten ps of
+  flatten (F.PAnd exprs) = case flatten exprs of
                          [p] -> p
                          ps  -> F.PAnd ps
   flatten p = p
@@ -1018,16 +1017,16 @@
 -- | Split heads into one for each kvar so that queries are always horn constraints
 hornify :: Cstr a -> Cstr a
 hornify (Head (PAnd ps) a) = CAnd (flip Head a <$> ps')
-  where ps' = let (ks, qs) = split [] [] (flatten ps) in PAnd qs : ks
+  where ps' = let (ks, qs) = splitP [] [] (flatten ps) in PAnd qs : ks
 
-        split kacc pacc ((Var x xs):qs) = split (Var x xs : kacc) pacc qs
-        split kacc pacc (q:qs) = split kacc (q:pacc) qs
-        split kacc pacc [] = (kacc, pacc)
-hornify (Head (Reft r) a) = CAnd (flip Head a <$> (Reft (F.PAnd ps):(Reft <$> ks)))
-  where (ks, ps) = split [] [] $ F.splitPAnd r
-        split kacc pacc (r@F.PKVar{}:rs) = split (r:kacc) pacc rs
-        split kacc pacc (r:rs) = split kacc (r:pacc) rs
-        split kacc pacc [] = (kacc,pacc)
+        splitP kacc pacc ((Var x xs):qs) = splitP (Var x xs : kacc) pacc qs
+        splitP kacc pacc (q:qs) = splitP kacc (q:pacc) qs
+        splitP kacc pacc [] = (kacc, pacc)
+hornify (Head (Reft expr) a) = CAnd (flip Head a <$> (Reft (F.PAnd ps):(Reft <$> ks)))
+  where (ks, ps) = splitP [] [] $ F.splitPAnd expr
+        splitP kacc pacc (r@F.PKVar{}:rs) = splitP (r:kacc) pacc rs
+        splitP kacc pacc (r:rs) = splitP kacc (r:pacc) rs
+        splitP kacc pacc [] = (kacc,pacc)
 hornify (Head h a) = Head h a
 hornify (All b c) = All b $ hornify c
 hornify (Any b c) = Any b $ hornify c
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
@@ -9,8 +9,6 @@
 {-# LANGUAGE DeriveGeneric              #-}
 {-# LANGUAGE DeriveTraversable          #-}
 
-{-# OPTIONS_GHC -Wno-name-shadowing #-}
-
 module Language.Fixpoint.Horn.Types
   ( -- * Horn Constraints and their components
     Query (..)
@@ -231,13 +229,13 @@
   toJSON (Tag s) = String (T.pack s)
 
 instance F.PPrint (Query a) where
-  pprintPrec k t q = P.vcat $ L.intersperse " "
+  pprintPrec prec t q = P.vcat $ L.intersperse " "
     [ P.vcat   (ppQual <$> qQuals q)
     , P.vcat   [ppVar k   | k <- qVars q]
-    , P.vcat   [ppCon x t | (x, t) <- M.toList (qCon q)]
+    , P.vcat   [ppCon x sort' | (x, sort') <- M.toList (qCon q)]
     , ppThings Nothing (qEqns  q)
     , ppThings (Just "data ") (qData  q)
-    , P.parens (P.vcat ["constraint", F.pprintPrec (k+2) t (qCstr q)])
+    , P.parens (P.vcat ["constraint", F.pprintPrec (prec+2) t (qCstr q)])
     ]
 
 ppThings :: F.PPrint a => Maybe P.Doc -> [a] -> P.Doc
diff --git a/src/Language/Fixpoint/Minimize.hs b/src/Language/Fixpoint/Minimize.hs
--- a/src/Language/Fixpoint/Minimize.hs
+++ b/src/Language/Fixpoint/Minimize.hs
@@ -7,8 +7,6 @@
 
 {-# LANGUAGE ScopedTypeVariables #-}
 
-{-# OPTIONS_GHC -Wno-name-shadowing #-}
-
 module Language.Fixpoint.Minimize ( minQuery, minQuals, minKvars ) where
 
 import Prelude hiding (min, init)
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
@@ -5,8 +5,6 @@
 {-# LANGUAGE DeriveGeneric             #-}
 {-# LANGUAGE OverloadedStrings         #-}
 
-{-# OPTIONS_GHC -Wno-name-shadowing #-}
-
 module Language.Fixpoint.Parse (
 
   -- * Top Level Class for Parseable Values
@@ -1026,9 +1024,9 @@
   <|> (mkFTycon          =<<  locUpperIdP)
 
 mkFTycon :: LocSymbol -> Parser FTycon
-mkFTycon locSym = do
+mkFTycon locSymbol = do
   nums  <- gets numTyCons
-  return (symbolNumInfoFTyCon locSym (val locSym `S.member` nums) False)
+  return (symbolNumInfoFTyCon locSymbol (val locSymbol `S.member` nums) False)
 
 
 --------------------------------------------------------------------------------
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
@@ -8,8 +8,6 @@
 {-# LANGUAGE PatternGuards             #-}
 {-# LANGUAGE DoAndIfThenElse           #-}
 
-{-# OPTIONS_GHC -Wno-name-shadowing #-}
-
 -- | This module contains an SMTLIB2 interface for
 --   1. checking the validity, and,
 --   2. computing satisfying assignments
@@ -272,17 +270,17 @@
   -> Process.Config
   -> IO (SMTLIB.Backends.Backend, IO ())
 makeProcess ctxLog cfg
-  = do handle@Process.Handle {hMaybeErr = Just hErr, ..} <- Process.new cfg
+  = do handl@Process.Handle {hMaybeErr = Just hErr, ..} <- Process.new cfg
        case ctxLog of
          Nothing -> return ()
          Just hLog -> void $ async $ forever
-           (do err <- LTIO.hGetLine hErr
-               LTIO.hPutStrLn hLog $ "OOPS, SMT solver error:" <> err
+           (do errTxt <- LTIO.hGetLine hErr
+               LTIO.hPutStrLn hLog $ "OOPS, SMT solver error:" <> errTxt
            ) `catch` \ SomeException {} -> return ()
-       let backend = Process.toBackend handle
+       let backend = Process.toBackend handl
        hSetBuffering hOut $ BlockBuffering $ Just $ 1024 * 1024 * 64
        hSetBuffering hIn $ BlockBuffering $ Just $ 1024 * 1024 * 64
-       return (backend, Process.close handle)
+       return (backend, Process.close handl)
 
 makeContext' :: Config -> Maybe Handle -> IO Context
 makeContext' cfg ctxLog
@@ -399,12 +397,12 @@
 smtAssert me p  = interact' me (Assert Nothing p)
 
 smtDefineFunc :: Context -> Symbol -> [(Symbol, F.Sort)] -> F.Sort -> Expr -> IO ()
-smtDefineFunc me name params rsort e =
+smtDefineFunc me name symList rsort e =
   let env = seData (ctxSymEnv me)
    in interact' me $
         DefineFunc
           name
-          (map (sortSmtSort False env <$>) params)
+          (map (sortSmtSort False env <$>) symList)
           (sortSmtSort False env rsort)
           e
 
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
@@ -6,7 +6,6 @@
 {-# LANGUAGE DoAndIfThenElse      #-}
 
 {-# OPTIONS_GHC -Wno-orphans        #-}
-{-# OPTIONS_GHC -Wno-name-shadowing #-}
 
 -- | This module contains the code for serializing Haskell values
 --   into SMTLIB2 format, that is, the instances for the @SMTLIB2@
@@ -153,9 +152,9 @@
   smt2 env (PImp p q)       = parenSeqs ["=>", smt2 env p, smt2 env q]
   smt2 env (PIff p q)       = parenSeqs ["=", smt2 env p, smt2 env q]
   smt2 env (PExist [] p)    = smt2 env p
-  smt2 env (PExist bs p)    = parenSeqs ["exists", parens (smt2s env bs), smt2 env p]
+  smt2 env (PExist xs p)    = parenSeqs ["exists", parens (smt2s env xs), smt2 env p]
   smt2 env (PAll   [] p)    = smt2 env p
-  smt2 env (PAll   bs p)    = parenSeqs ["forall", parens (smt2s env bs), smt2 env p]
+  smt2 env (PAll   xs p)    = parenSeqs ["forall", parens (smt2s env xs), smt2 env p]
   smt2 env (PAtom r e1 e2)  = mkRel env r e1 e2
   smt2 env (ELam b e)       = smt2Lam   env b e
   smt2 env (ECoerc t1 t2 e) = smt2Coerc env t1 t2 e
@@ -231,8 +230,8 @@
   smt2 env (DeclData ds)       = key "declare-datatypes" (smt2data env ds)
   smt2 env (Declare x ts t)    = parenSeqs ["declare-fun", Builder.fromText x, parens (smt2many (smt2 env <$> ts)), smt2 env t]
   smt2 env c@(Define t)        = key "declare-sort" (smt2SortMono c env t)
-  smt2 env (DefineFunc name params rsort e) =
-    let bParams = [ parenSeqs [smt2 env s, smt2 env t] | (s, t) <- params]
+  smt2 env (DefineFunc name paramxs rsort e) =
+    let bParams = [ parenSeqs [smt2 env s, smt2 env t] | (s, t) <- paramxs]
      in parenSeqs ["define-fun", smt2 env name, parenSeqs bParams, smt2 env rsort, smt2 env e]
   smt2 env (Assert Nothing p)  = {-# SCC "smt2-assert" #-} key "assert" (smt2 env p)
   smt2 env (Assert (Just i) p) = {-# SCC "smt2-assert" #-} key "assert" (parens ("!"<+> smt2 env p <+> ":named p-" <> bShow i))
@@ -251,14 +250,14 @@
 instance SMTLIB2 (Triggered Expr) where
   smt2 env (TR NoTrigger e)       = smt2 env e
   smt2 env (TR _ (PExist [] p))   = smt2 env p
-  smt2 env t@(TR _ (PExist bs p)) = smtTr env "exists" bs p t
+  smt2 env t@(TR _ (PExist xs p)) = smtTr env "exists" xs p t
   smt2 env (TR _ (PAll   [] p))   = smt2 env p
-  smt2 env t@(TR _ (PAll   bs p)) = smtTr env "forall" bs p t
+  smt2 env t@(TR _ (PAll   xs p)) = smtTr env "forall" xs p t
   smt2 env (TR _ e)               = smt2 env e
 
 {-# INLINE smtTr #-}
 smtTr :: SymEnv -> Builder -> [(Symbol, Sort)] -> Expr -> Triggered Expr -> Builder
-smtTr env q bs p t = key q (parens (smt2s env bs) <+> key "!" (smt2 env p <+> ":pattern" <> parens (smt2s env (makeTriggers t))))
+smtTr env q xs p t = key q (parens (smt2s env xs) <+> key "!" (smt2 env p <+> ":pattern" <> parens (smt2s env (makeTriggers t))))
 
 {-# INLINE smt2s #-}
 smt2s    :: SMTLIB2 a => SymEnv -> [a] -> Builder
diff --git a/src/Language/Fixpoint/Smt/Theories.hs b/src/Language/Fixpoint/Smt/Theories.hs
--- a/src/Language/Fixpoint/Smt/Theories.hs
+++ b/src/Language/Fixpoint/Smt/Theories.hs
@@ -7,7 +7,6 @@
 {-# LANGUAGE ViewPatterns              #-}
 
 {-# OPTIONS_GHC -Wno-orphans           #-}
-{-# OPTIONS_GHC -Wno-name-shadowing    #-}
 
 module Language.Fixpoint.Smt.Theories
      (
@@ -443,9 +442,9 @@
   | f == setEmp   = Just (key2 "=" (fromText emp) d)
   | f == setSng   = Just (key (fromText sng) d) -- Just (key2 (bb add) (bb emp) d)
 
-smt2App k env f (d:ds)
+smt2App k env f (builder:builders)
   | Just fb <- smt2AppArg k env f
-  = Just $ key fb (d <> mconcat [ " " <> d | d <- ds])
+  = Just $ key fb (builder <> mconcat [ " " <> d | d <- builders])
 
 smt2App _ _ _ _    = Nothing
 
diff --git a/src/Language/Fixpoint/Smt/Types.hs b/src/Language/Fixpoint/Smt/Types.hs
--- a/src/Language/Fixpoint/Smt/Types.hs
+++ b/src/Language/Fixpoint/Smt/Types.hs
@@ -4,7 +4,6 @@
 {-# LANGUAGE OverloadedStrings         #-}
 {-# LANGUAGE UndecidableInstances      #-}
 
-{-# OPTIONS_GHC -Wno-name-shadowing    #-}
 
 -- | This module contains the types defining an SMTLIB2 interface.
 
@@ -74,8 +73,8 @@
 ppCmd (Declare x [] t) = text "Declare" <+> text (T.unpack x) <+> text ":" <+> pprint t
 ppCmd (Declare x ts t) = text "Declare" <+> text (T.unpack x) <+> text ":" <+> parens (pprint ts) <+> pprint t
 ppCmd Define {}   = text "Define ..."
-ppCmd (DefineFunc name params rsort e) =
-  text "DefineFunc" <+> pprint name <+> pprint params <+> pprint rsort <+> pprint e
+ppCmd (DefineFunc name symList rsort e) =
+  text "DefineFunc" <+> pprint name <+> pprint symList <+> pprint rsort <+> pprint e
 ppCmd (Assert _ e)  = text "Assert" <+> pprint e
 ppCmd (AssertAx _)  = text "AssertAxiom ..."
 ppCmd Distinct {} = text "Distinct ..."
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
@@ -6,8 +6,6 @@
 {-# LANGUAGE OverloadedStrings   #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
-{-# OPTIONS_GHC -Wno-name-shadowing #-}
-
 module Language.Fixpoint.Solver (
     -- * Invoke Solver on an FInfo
     solve, Solver
@@ -188,11 +186,11 @@
                              (return . crashResult (errorMap fi0))
 
 crashResult :: (PPrint a) => ErrorMap a -> Error -> Result (Integer, a)
-crashResult m e = Result res mempty mempty mempty
+crashResult m err' = Result res mempty mempty mempty
   where
     res           = Crash es msg
-    es            = catMaybes [ findError m e | e <- errs e ]
-    msg | null es = showpp e
+    es            = catMaybes [ findError m e | e <- errs err' ]
+    msg | null es = showpp err'
         | otherwise = "Sorry, unexpected panic in liquid-fixpoint!" -- ++ showpp e
 
 -- | Unpleasant hack to save meta-data that can be recovered from SrcSpan
diff --git a/src/Language/Fixpoint/Solver/Common.hs b/src/Language/Fixpoint/Solver/Common.hs
--- a/src/Language/Fixpoint/Solver/Common.hs
+++ b/src/Language/Fixpoint/Solver/Common.hs
@@ -1,7 +1,5 @@
 {-# LANGUAGE OverloadedStrings #-}
 
-{-# OPTIONS_GHC -Wno-name-shadowing #-}
-
 module Language.Fixpoint.Solver.Common (askSMT, toSMT) where
 
 import Language.Fixpoint.Types.Config (Config)
@@ -15,20 +13,20 @@
 mytracepp = notracepp
 
 askSMT :: Config -> Context -> [(Symbol, Sort)] -> Expr -> IO Bool
-askSMT cfg ctx bs e
+askSMT cfg ctx xs e
 --   | isContraPred e  = return False
   | isTautoPred  e     = return True
   | null (kvarsExpr e) = checkValidWithContext ctx [] PTrue e'
   | otherwise          = return False
   where
-    e' = toSMT "askSMT" cfg ctx bs e
+    e' = toSMT "askSMT" cfg ctx xs e
 
 toSMT :: String -> Config -> Context -> [(Symbol, Sort)] -> Expr -> Pred
-toSMT msg cfg ctx bs e =
-    defuncAny cfg senv .
-        elaborate (dummyLoc msg) (elabEnv bs) .
+toSMT msg cfg ctx xs e =
+    defuncAny cfg symenv .
+        elaborate (dummyLoc msg) (elabEnv xs) .
             mytracepp ("toSMT from " ++ msg ++ showpp e) $
                 e
   where
-    elabEnv = insertsSymEnv senv
-    senv    = ctxSymEnv ctx
+    elabEnv = insertsSymEnv symenv
+    symenv  = ctxSymEnv ctx
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
@@ -6,8 +6,6 @@
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE TupleSections #-}
 
-{-# OPTIONS_GHC -Wno-name-shadowing #-}
-
 -- | Functions to make environments smaller
 module Language.Fixpoint.Solver.EnvironmentReduction
   ( reduceEnvironments
@@ -136,19 +134,19 @@
 -- See #473 for more discussion.
 --
 reduceEnvironments :: FInfo a -> FInfo a
-reduceEnvironments fi =
-  let constraints = HashMap.Strict.toList $ cm fi
-      aenvMap = axiomEnvSymbols (ae fi)
-      reducedEnvs = map (reduceConstraintEnvironment (bs fi) aenvMap) constraints
-      (cm', ws') = reduceWFConstraintEnvironments (bs fi) (reducedEnvs, ws fi)
-      bs' = (bs fi) { beBinds = dropBindsMissingFrom (beBinds $ bs fi) cm' ws' }
+reduceEnvironments finfo =
+  let constraints = HashMap.Strict.toList $ cm finfo
+      aenvMap = axiomEnvSymbols (ae finfo)
+      reducedEnvs = map (reduceConstraintEnvironment (bs finfo) aenvMap) constraints
+      (cm', ws') = reduceWFConstraintEnvironments (bs finfo) (reducedEnvs, ws finfo)
+      bs' = (bs finfo) { beBinds = dropBindsMissingFrom (beBinds $ bs finfo) cm' ws' }
 
-   in fi
+   in finfo
      { bs = bs'
      , cm = HashMap.fromList cm'
      , ws = ws'
-     , ebinds = updateEbinds bs' (ebinds fi)
-     , bindInfo = updateBindInfoKeys bs' $ bindInfo fi
+     , ebinds = updateEbinds bs' (ebinds finfo)
+     , bindInfo = updateBindInfoKeys bs' $ bindInfo finfo
      }
 
   where
@@ -157,10 +155,10 @@
       -> [(SubcId, SubC a)]
       -> HashMap KVar (WfC a)
       -> HashMap BindId (Symbol, SortedReft, a)
-    dropBindsMissingFrom be cs ws =
+    dropBindsMissingFrom be cs wmap =
       let ibindEnv = unionsIBindEnv $
             map (senv . snd) cs ++
-            map wenv (HashMap.elems ws)
+            map wenv (HashMap.elems wmap)
        in
           HashMap.filterWithKey (\bId _ -> memberIBindEnv bId ibindEnv) be
 
@@ -200,7 +198,7 @@
 
       ws' =
         HashMap.mapWithKey
-          (reduceWFConstraintEnvironment bindEnv kvarsRelevantBinds)
+          (reduceWFConstraintEnvironment kvarsRelevantBinds)
           wfs
 
       wsSymbols = HashMap.map (asSymbolSet bindEnv . wenv) ws'
@@ -209,7 +207,7 @@
         HashMap.unionWith HashSet.intersection wfBindsPlusSortSymbols wsSymbols
 
       cs' = zipWith
-              (updateSubcEnvsWithKVarBinds bindEnv kvarsWsBinds)
+              (updateSubcEnvsWithKVarBinds kvarsWsBinds)
               kvarsBySubC
               cs
    in
@@ -221,23 +219,22 @@
     -- additional bindings that are required by the kvar. These are added
     -- in this function.
     updateSubcEnvsWithKVarBinds
-      :: BindEnv a
-      -> HashMap KVar (HashSet Symbol)
+      :: HashMap KVar (HashSet Symbol)
       -> [KVar]
       -> ReducedConstraint a
       -> (SubcId, SubC a)
-    updateSubcEnvsWithKVarBinds be kvarsBinds kvs c =
+    updateSubcEnvsWithKVarBinds kvarsBinds kvs c =
       let updateIBindEnv oldEnv =
             unionIBindEnv (reducedEnv c) $
             if null kvs then emptyIBindEnv
             else fromListIBindEnv
               [ bId
               | bId <- elemsIBindEnv oldEnv
-              , let (s, _sr, _) = lookupBindEnv bId be
+              , let (s, _sr, _) = lookupBindEnv bId bindEnv
               , any (neededByKVar s) kvs
               ]
-          neededByKVar s kv =
-            case HashMap.lookup kv kvarsBinds of
+          neededByKVar s kvar =
+            case HashMap.lookup kvar kvarsBinds of
               Nothing -> False
               Just kbindSyms -> HashSet.member s kbindSyms
        in (constraintId c, updateSEnv (originalConstraint c) updateIBindEnv)
@@ -245,12 +242,11 @@
     -- @reduceWFConstraintEnvironment be kbinds k c@ drops bindings from @c@
     -- that aren't present in @kbinds ! k@.
     reduceWFConstraintEnvironment
-      :: BindEnv a
-      -> HashMap KVar (HashSet Symbol)
+      :: HashMap KVar (HashSet Symbol)
       -> KVar
       -> WfC a
       -> WfC a
-    reduceWFConstraintEnvironment bindEnv kvarBinds k c =
+    reduceWFConstraintEnvironment kvarBinds k c =
       case HashMap.lookup k kvarBinds of
         Nothing -> c { wenv = emptyIBindEnv }
         Just kbindSymbols ->
@@ -320,10 +316,10 @@
 
 -- | For each Equation and Rewrite, collects the symbols that it needs.
 axiomEnvSymbols :: AxiomEnv -> HashMap Symbol (HashSet Symbol)
-axiomEnvSymbols ae =
+axiomEnvSymbols axiomEnv =
   HashMap.union
-    (HashMap.fromList $ map eqSymbols $ aenvEqs ae)
-    (HashMap.fromList $ map rewriteSymbols $ aenvSimpl ae)
+    (HashMap.fromList $ map eqSymbols $ aenvEqs axiomEnv)
+    (HashMap.fromList $ map rewriteSymbols $ aenvSimpl axiomEnv)
   where
     eqSymbols eq =
       let bodySymbols =
@@ -461,13 +457,13 @@
 -- If 'inlineANFBindings cfg' is on, also runs 'undoANFAndVV' to inline
 -- @lq_anf@ bindings.
 simplifyBindings :: Config -> FInfo a -> FInfo a
-simplifyBindings cfg fi =
-  let (bs', cm', oldToNew) = simplifyConstraints (bs fi) (cm fi)
-   in fi
+simplifyBindings cfg finfo =
+  let (bs', cm', oldToNew) = simplifyConstraints (bs finfo) (cm finfo)
+   in finfo
         { bs = bs'
         , cm = cm'
-        , ebinds = updateEbinds oldToNew (ebinds fi)
-        , bindInfo = updateBindInfoKeys oldToNew $ bindInfo fi
+        , ebinds = updateEbinds oldToNew (ebinds finfo)
+        , bindInfo = updateBindInfoKeys oldToNew $ bindInfo finfo
         }
   where
     updateEbinds :: HashMap BindId [BindId] -> [BindId] -> [BindId]
@@ -518,7 +514,7 @@
 
           modifiedBinds = HashMap.toList $ HashMap.union boolSimplEnv undoANFEnv
 
-          modifiedBindIds = [ fst <$> bs | (_, (bs,_)) <- modifiedBinds ]
+          modifiedBindIds = [ fst <$> bindIds | (_, (bindIds,_)) <- modifiedBinds ]
 
           unchangedBindIds = senv c `diffIBindEnv` fromListIBindEnv (concat modifiedBindIds)
 
@@ -632,10 +628,10 @@
   -> SortedReft
   -> SortedReft
 inlineInSortedReft srLookup sr =
-    let reft = sr_reft sr
-     in sr { sr_reft = mapPredReft (inlineInExpr (filterBind (reftBind reft) srLookup)) reft }
+    let reft' = sr_reft sr
+     in sr { sr_reft = mapPredReft (inlineInExpr (filterBind (reftBind reft'))) reft' }
   where
-    filterBind b srLookup sym = do
+    filterBind b sym = do
       guard (sym /= b)
       srLookup sym
 
@@ -713,7 +709,7 @@
     findExpr e es = do
       case partition (e ==) es of
         ([], _) -> Nothing
-        (e:_, rest) -> Just (e, rest)
+        (f:_, rest) -> Just (f, rest)
 
 -- | @dropLikelyIrrelevantBindings ss env@ is like @dropIrrelevantBindings@
 -- but drops bindings that could potentially be necessary to validate a
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
@@ -3,7 +3,6 @@
 {-# LANGUAGE PatternGuards        #-}
 {-# LANGUAGE FlexibleContexts     #-}
 
-{-# OPTIONS_GHC -Wno-name-shadowing #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 
 module Language.Fixpoint.Solver.Extensionality (expand) where
@@ -58,22 +57,22 @@
 
 
 extendExpr :: a -> Pos -> Expr -> Ex a Expr
-extendExpr ann p e
+extendExpr ann p expr'
   | p == Pos
   = mapMPosExpr Pos goP e' >>= mapMPosExpr Pos goN
   | otherwise
   = mapMPosExpr Neg goP e' >>= mapMPosExpr Neg goN
     where
-      e' = normalize e
+      e' = normalize expr'
       goP Pos (PAtom b e1 e2)
        | b == Eq || b == Ne
        , Just s <- getArg (exprSort "extensionality" e1)
-       = mytracepp ("extending POS = " ++ showpp e) <$> (extendRHS ann b e1 e2 s >>= goP Pos)
+       = mytracepp ("extending POS = " ++ showpp expr') <$> (extendRHS ann b e1 e2 s >>= goP Pos)
       goP _ e = return e
       goN Neg (PAtom b e1 e2)
        | b == Eq || b == Ne
        , Just s <- getArg (exprSort "extensionality" e1)
-       = mytracepp ("extending NEG = " ++ showpp e) <$> (extendLHS ann b e1 e2 s >>= goN Neg)
+       = mytracepp ("extending NEG = " ++ showpp expr') <$> (extendLHS ann b e1 e2 s >>= goN Neg)
       goN _ e = return e
 
 getArg :: Sort -> Maybe Sort
@@ -93,9 +92,9 @@
      mytracepp "extendLHS = " . pAnd . (PAtom b e1 e2:) <$> mapM (makeEq b e1 e2) (es ++ is)
 
 generateArguments :: a -> Sort -> Ex a [Expr]
-generateArguments ann s = do
-  ddecls   <- gets exddecl
-  case breakSort ddecls s of
+generateArguments ann srt = do
+  ddatadecls <- gets exddecl
+  case breakSort ddatadecls srt of
     Left dds -> mapM (freshArgDD ann) dds
     Right s  -> (\x -> [EVar x]) <$> freshArgOne ann s
 
@@ -130,7 +129,7 @@
 negatePos Neg = Pos
 
 mapMPosExpr :: (Monad m) => Pos -> (Pos -> Expr -> m Expr) -> Expr -> m Expr
-mapMPosExpr p f = go p
+mapMPosExpr pos f = go pos
   where
     go p e@(ESym _)      = f p e
     go p e@(ECon _)      = f p e
@@ -161,7 +160,7 @@
     go p (PGrad k s i e) = f p . PGrad k s i =<< go p e
 
 normalize :: Expr -> Expr
-normalize e = mytracepp ("normalize: " ++ showpp e) $ go e
+normalize expr' = mytracepp ("normalize: " ++ showpp expr') $ go expr'
   where
     go e@(ESym _)        = e
     go e@(ECon _)        = e
@@ -224,19 +223,19 @@
 
 
 freshArgDD :: a -> (LocSymbol, [Sort]) -> Ex a Expr
-freshArgDD ann (dc, xs) = do
-  xs <- mapM (freshArgOne ann) xs
+freshArgDD ann (dc, sorts) = do
+  xs <- mapM (freshArgOne ann) sorts
   return $ mkEApp dc (EVar <$> xs)
 
 
 freshArgOne :: ann -> Sort -> Ex ann Symbol
 freshArgOne ann s = do
-  st   <- get
-  let x = symbol ("ext$" ++ show (unique st))
-  let (id, benv') = insertBindEnv x (trueSortedReft s) ann (exbenv st)
+  exst <- get
+  let x = symbol ("ext$" ++ show (unique exst))
+  let (bindId, benv') = insertBindEnv x (trueSortedReft s) ann (exbenv exst)
   modify (\st -> st{ exenv   = insertSymEnv x s (exenv st)
                    , exbenv  = benv'
-                   , exbinds = insertsIBindEnv [id] (exbinds st)
+                   , exbinds = insertsIBindEnv [bindId] (exbinds st)
                    , unique   = 1 + unique st
                    , excbs = (x,s) : excbs st
                    })
@@ -244,9 +243,9 @@
 
 
 breakSort :: [DataDecl] -> Sort -> Either [(LocSymbol, [Sort])] Sort
-breakSort ddecls s
+breakSort ddatadecls s
     | Just (tc, ts) <- splitTC s
-    , [(dds,i)] <- [ (ddCtors dd,ddVars dd) | dd <- ddecls, ddTyCon dd == tc ]
+    , [(dds,i)] <- [ (ddCtors dd,ddVars dd) | dd <- ddatadecls, ddTyCon dd == tc ]
     = Left ((\dd -> (dcName dd, instSort  (Sub $ zip [0..(i-1)] ts) . dfSort <$> dcFields dd)) <$> dds)
     | otherwise
     = Right s
diff --git a/src/Language/Fixpoint/Solver/GradualSolution.hs b/src/Language/Fixpoint/Solver/GradualSolution.hs
--- a/src/Language/Fixpoint/Solver/GradualSolution.hs
+++ b/src/Language/Fixpoint/Solver/GradualSolution.hs
@@ -1,8 +1,6 @@
 {-# LANGUAGE CPP                #-}
 {-# LANGUAGE FlexibleInstances  #-}
 
-{-# OPTIONS_GHC -Wno-name-shadowing #-}
-
 module Language.Fixpoint.Solver.GradualSolution
   ( -- * Create Initial Solution
     init
@@ -18,7 +16,7 @@
 import           Language.Fixpoint.Misc
 import qualified Language.Fixpoint.Types              as F
 import qualified Language.Fixpoint.Types.Solutions    as Sol
-import           Language.Fixpoint.Types.Constraints  hiding (ws, bs)
+import qualified Language.Fixpoint.Types.Constraints  as Cons
 import           Prelude                              hiding (init, lookup)
 import           Language.Fixpoint.Solver.Sanitize  (symbolEnv)
 import Language.Fixpoint.SortCheck
@@ -34,9 +32,9 @@
     gs         = snd <$> gs0
     genv       = instConstants si
 
-    gs0        = L.filter (isGWfc . snd) $ M.toList (F.ws si)
+    gs0        = L.filter (Cons.isGWfc . snd) $ M.toList (F.ws si)
 
-    elab (k, (x,es)) = (k, (x, elaborate (F.atLoc F.dummySpan "init") (sEnv (gsym x) (gsort x)) <$> es))
+    elab (k, (x,es)) = (k, (x, elaborate (F.atLoc F.dummySpan "init") (sEnv (Cons.gsym x) (Cons.gsort x)) <$> es))
 
     sEnv x s    = isEnv {F.seSort = F.insertSEnv x s (F.seSort isEnv)}
     isEnv       = symbolEnv cfg si
@@ -49,7 +47,7 @@
     (k, qb) = refine fi qs genv w
 
 refine :: F.SInfo a -> [F.Qualifier] -> F.SEnv F.Sort -> F.WfC a -> (F.KVar, Sol.QBind)
-refine fi qs genv w = refineK (allowHOquals fi) env qs $ F.wrft w
+refine fi qs genv w = refineK (Cons.allowHOquals fi) env qs $ F.wrft w
   where
     env             = wenv <> genv
     wenv            = F.sr_sort <$> F.fromListSEnv (F.envCs (F.bs fi) (F.wenv w))
@@ -85,7 +83,7 @@
        -> F.Qualifier
        -> [Sol.EQual]
 instKQ ho env v t q =
-  case qpSort <$> F.qParams q of
+  case Cons.qpSort <$> F.qParams q of
     (qt:qts) -> do
         (su0, v0) <- candidates senv [(t, [v])] qt
         xs        <- match senv tyss [v0] (So.apply su0 <$> qts)
diff --git a/src/Language/Fixpoint/Solver/Instantiate.hs b/src/Language/Fixpoint/Solver/Instantiate.hs
--- a/src/Language/Fixpoint/Solver/Instantiate.hs
+++ b/src/Language/Fixpoint/Solver/Instantiate.hs
@@ -17,8 +17,6 @@
 {-# LANGUAGE RecordWildCards           #-}
 {-# LANGUAGE ExistentialQuantification #-}
 
-{-# OPTIONS_GHC -Wno-name-shadowing    #-}
-
 module Language.Fixpoint.Solver.Instantiate (instantiate) where
 
 import           Language.Fixpoint.Types
@@ -54,15 +52,15 @@
 -- | Strengthen Constraint Environments via PLE
 --------------------------------------------------------------------------------
 instantiate :: (Loc a) => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
-instantiate cfg fi subcIds
+instantiate cfg info subcIds
   | not (oldPLE cfg)
-  = PLE.instantiate cfg fi subcIds
+  = PLE.instantiate cfg info subcIds
 
   | noIncrPle cfg
-  = instantiate' cfg fi subcIds
+  = instantiate' cfg info subcIds
 
   | otherwise
-  = incrInstantiate' cfg fi subcIds
+  = incrInstantiate' cfg info subcIds
 
 
 -------------------------------------------------------------------------------
@@ -79,27 +77,27 @@
 -------------------------------------------------------------------------------
 incrInstantiate' :: (Loc a) => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
 -------------------------------------------------------------------------------
-incrInstantiate' cfg fi subcIds = do
-    let cs = [ (i, c) | (i, c) <- M.toList (cm fi), isPleCstr aEnv i c
+incrInstantiate' cfg info subcIds = do
+    let cs = [ (i, c) | (i, c) <- M.toList (cm info), isPleCstr aEnv i c
                       ,  maybe True (i `L.elem`) subcIds ]
     let t  = mkCTrie cs                                               -- 1. BUILD the Trie
     res   <- withProgress (1 + length cs) $
-               withCtx cfg file sEnv (pleTrie t . instEnv cfg fi cs)  -- 2. TRAVERSE Trie to compute InstRes
-    return $ resSInfo cfg sEnv fi res                                 -- 3. STRENGTHEN SInfo using InstRes
+               withCtx cfg file sEnv (pleTrie t . instEnv cfg info cs)  -- 2. TRAVERSE Trie to compute InstRes
+    return $ resSInfo cfg sEnv info res                                 -- 3. STRENGTHEN SInfo using InstRes
   where
     file   = srcFile cfg ++ ".evals"
-    sEnv   = symbolEnv cfg fi
-    aEnv   = ae fi
+    sEnv   = symbolEnv cfg info
+    aEnv   = ae info
 
 
 
 -------------------------------------------------------------------------------
 -- | Step 1a: @instEnv@ sets up the incremental-PLE environment
 instEnv :: (Loc a) => Config -> SInfo a -> [(SubcId, SimpC a)] -> SMT.Context -> InstEnv a
-instEnv cfg fi cs ctx = InstEnv cfg ctx bEnv aEnv (M.fromList cs) γ s0
+instEnv cfg info cs ctx = InstEnv cfg ctx bEnv aEnv (M.fromList cs) γ s0
   where
-    bEnv              = bs fi
-    aEnv              = ae fi
+    bEnv              = bs info
+    aEnv              = ae info
     γ                 = knowledge cfg ctx aEnv
     s0                = EvalEnv 0 [] aEnv (SMT.ctxSymEnv ctx) cfg
 
@@ -161,7 +159,7 @@
 unfoldPred cfg ctx = toSMT cfg ctx [] . pAnd . concatMap snd
 
 evalCandsLoop :: Config -> SMT.Context -> Knowledge -> EvalEnv -> [Expr] -> IO [Unfold]
-evalCandsLoop cfg ctx γ s0 cands = go [] cands
+evalCandsLoop cfg ctx γ s0 = go []
   where
     go acc []    = return acc
     go acc cands = do eqss   <- SMT.smtBracket ctx "PLE.evaluate" $ do
@@ -180,7 +178,7 @@
 -- | Step 3: @resSInfo@ uses incremental PLE result @InstRes@ to produce the strengthened SInfo
 
 resSInfo :: Config -> SymEnv -> SInfo a -> InstRes -> SInfo a
-resSInfo cfg env fi res = strengthenBinds fi res'
+resSInfo cfg env info res = strengthenBinds info res'
   where
     res'     = M.fromList $ mytracepp  "ELAB-INST:  " $ zip is ps''
     ps''     = zipWith (\i -> elaborate (atLoc dummySpan ("PLE1 " ++ show i)) env) is ps'
@@ -258,11 +256,11 @@
                ]
 
 debugResult :: InstEnv a -> InstRes -> SubcId -> String
-debugResult InstEnv{..} res i = msg
+debugResult InstEnv{..} res subId = msg
   where
-    msg                          = "INCR-INSTANTIATE i = " ++ show i ++ ": " ++ showpp cidEqs
+    msg                          = "INCR-INSTANTIATE i = " ++ show subId ++ ": " ++ showpp cidEqs
     cidEqs                       = pAnd [ e | i <- cBinds, e <- Mb.maybeToList $ M.lookup i res ]
-    cBinds                       = L.sort . elemsIBindEnv . senv . getCstr ieCstrs $ i
+    cBinds                       = L.sort . elemsIBindEnv . senv . getCstr ieCstrs $ subId
 
 
 updRes :: InstRes -> Maybe BindId -> Expr -> InstRes
@@ -298,35 +296,35 @@
 -- | "Old" GLOBAL PLE
 --------------------------------------------------------------------------------
 instantiate' :: (Loc a) => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
-instantiate' cfg fi subcIds = sInfo cfg env fi <$> withCtx cfg file env act
+instantiate' cfg info subcIds = sInfo cfg env info <$> withCtx cfg file env act
   where
     act ctx         = forM cstrs $ \(i, c) ->
-                        ((i,srcSpan c),) . mytracepp  ("INSTANTIATE i = " ++ show i) <$> instSimpC cfg ctx (bs fi) aenv i c
-    cstrs           = [ (i, c) | (i, c) <- M.toList (cm fi) , isPleCstr aenv i c
+                        ((i,srcSpan c),) . mytracepp  ("INSTANTIATE i = " ++ show i) <$> instSimpC cfg ctx (bs info) aenv i c
+    cstrs           = [ (i, c) | (i, c) <- M.toList (cm info) , isPleCstr aenv i c
                                ,  maybe True (i `L.elem`) subcIds ]
     file            = srcFile cfg ++ ".evals"
-    env             = symbolEnv cfg fi
-    aenv            = {- mytracepp  "AXIOM-ENV" -} ae fi
+    env             = symbolEnv cfg info
+    aenv            = {- mytracepp  "AXIOM-ENV" -} ae info
 
 sInfo :: Config -> SymEnv -> SInfo a -> [((SubcId, SrcSpan), Expr)] -> SInfo a
-sInfo cfg env fi ips = strengthenHyp fi (mytracepp  "ELAB-INST:  " $ zip (fst <$> is) ps'')
+sInfo cfg env info ips = strengthenHyp info (mytracepp  "ELAB-INST:  " $ zip (fst <$> is) ps'')
   where
     (is, ps)         = unzip ips
     ps'              = defuncAny cfg env ps
     ps''             = zipWith (\(i, sp) -> elaborate (atLoc sp ("PLE1 " ++ show i)) env) is ps'
 
 instSimpC :: Config -> SMT.Context -> BindEnv a -> AxiomEnv -> SubcId -> SimpC a -> IO Expr
-instSimpC cfg ctx bds aenv sid sub
-  | isPleCstr aenv sid sub = do
+instSimpC cfg ctx bds aenv subId sub
+  | isPleCstr aenv subId sub = do
     let is0       = mytracepp  "INITIAL-STUFF" $ eqBody <$> L.filter (null . eqArgs) (aenvEqs aenv)
     let (bs, es0) = cstrExprs bds sub
-    equalities   <- evaluate cfg ctx aenv bs es0 sid
+    equalities   <- evaluate cfg ctx aenv bs es0 subId
     let evalEqs   = [ EEq e1 e2 | (e1, e2) <- equalities, e1 /= e2 ]
     return        $ pAnd (is0 ++ evalEqs)
   | otherwise     = return PTrue
 
 isPleCstr :: AxiomEnv -> SubcId -> SimpC a -> Bool
-isPleCstr aenv sid c = isTarget c && M.lookupDefault False sid (aenvExpand aenv)
+isPleCstr aenv subId c = isTarget c && M.lookupDefault False subId (aenvExpand aenv)
 
 cstrExprs :: BindEnv a -> SimpC a -> ([(Symbol, SortedReft)], [Expr])
 cstrExprs bds sub = (second unElabSortedReft <$> binds, unElab <$> es)
@@ -343,10 +341,10 @@
          -> SubcId                            -- ^ Constraint Id
          -> IO [(Expr, Expr)]                 -- ^ Newly unfolded equalities
 --------------------------------------------------------------------------------
-evaluate cfg ctx aenv facts es sid = do
+evaluate cfg ctx aenv facts es subId = do
   let eqs      = initEqualities ctx aenv facts
   let γ        = knowledge cfg ctx aenv
-  let cands    = mytracepp  ("evaluate-cands " ++ showpp sid) $ Misc.setNub (concatMap topApps es)
+  let cands    = mytracepp  ("evaluate-cands " ++ showpp subId) $ Misc.setNub (concatMap topApps es)
   let s0       = EvalEnv 0 [] aenv (SMT.ctxSymEnv ctx) cfg
   let ctxEqs   = [ toSMT cfg ctx [] (EEq e1 e2) | (e1, e2)  <- eqs ]
               ++ [ toSMT cfg ctx [] (expr xr)   | xr@(_, r) <- facts, null (Vis.kvarsExpr $ reftPred $ sr_reft r) ]
@@ -356,7 +354,7 @@
 
 
 _evalLoop :: Config -> SMT.Context -> Knowledge -> EvalEnv -> [Pred] -> [Expr] -> IO [(Expr, Expr)]
-_evalLoop cfg ctx γ s0 ctxEqs cands = loop 0 [] cands
+_evalLoop cfg ctx γ s0 ctxEqs = loop 0 []
   where
     loop _ acc []    = return acc
     loop i acc cands = do let eqp = toSMT cfg ctx [] $ pAnd $ equalitiesPred acc
@@ -463,7 +461,7 @@
 --   TODO: distill a .fq test from the MOSSAKA-hw3 example.
 
 evalArgs :: Knowledge -> CStack -> Expr -> EvalST (Expr, [Expr])
-evalArgs γ stk e = go [] e
+evalArgs γ stk = go []
   where
     go acc (EApp f e)
       = do f' <- evalOk γ stk f
@@ -565,14 +563,14 @@
 mkCoSub :: SEnv Sort -> [Sort] -> [Sort] -> Vis.CoSub
 mkCoSub env eTs xTs = M.fromList [ (x, unite ys) | (x, ys) <- Misc.groupList xys ]
   where
-    unite ts    = mytracepp ("UNITE: " ++ showpp ts) $ Mb.fromMaybe (uError ts) (unifyTo1 senv ts)
-    senv        = mkSearchEnv env
+    unite ts    = mytracepp ("UNITE: " ++ showpp ts) $ Mb.fromMaybe (uError ts) (unifyTo1 symToSearch ts)
+    symToSearch = mkSearchEnv env
     uError ts   = panic ("mkCoSub: cannot build CoSub for " ++ showpp xys ++ " cannot unify " ++ showpp ts)
     xys         = mytracepp "mkCoSubXXX" $ Misc.sortNub $ concat $ zipWith matchSorts _xTs _eTs
     (_xTs,_eTs) = mytracepp "mkCoSub:MATCH" (xTs, eTs)
 
 matchSorts :: Sort -> Sort -> [(Symbol, Sort)]
-matchSorts s1 s2 = mytracepp  ("matchSorts :" ++ showpp (s1, s2)) $ go s1 s2
+matchSorts sort1 sort2 = mytracepp  ("matchSorts :" ++ showpp (sort1, sort2)) $ go sort1 sort2
   where
     go (FObj x)      {-FObj-} y    = [(x, y)]
     go (FAbs _ t1)   (FAbs _ t2)   = go t1 t2
@@ -603,7 +601,7 @@
 eqArgNames = map fst . eqArgs
 
 substPopIf :: [(Symbol, Expr)] -> Expr -> Expr
-substPopIf xes e = L.foldl' go e xes
+substPopIf xes expr' = L.foldl' go expr' xes
   where
     go e (x, EIte b e1 e2) = EIte b (subst1 e (x, e1)) (subst1 e (x, e2))
     go e (x, ex)           = subst1 e (x, ex)
@@ -695,9 +693,9 @@
 initEqualities :: SMT.Context -> AxiomEnv -> [(Symbol, SortedReft)] -> [(Expr, Expr)]
 initEqualities ctx aenv es = concatMap (makeSimplifications (aenvSimpl aenv)) dcEqs
   where
-    dcEqs                  = Misc.setNub (Mb.catMaybes [getDCEquality senv e1 e2 | EEq e1 e2 <- atoms])
+    dcEqs                  = Misc.setNub (Mb.catMaybes [getDCEquality symEnv' e1 e2 | EEq e1 e2 <- atoms])
     atoms                  = splitPAnd . expr =<< filter isProof es
-    senv                   = SMT.ctxSymEnv ctx
+    symEnv'                = SMT.ctxSymEnv ctx
 
 -- AT: Non-obvious needed invariant: askSMT True is always the
 -- totality-effecting one.
@@ -717,7 +715,7 @@
      = []
 
 getDCEquality :: SymEnv -> Expr -> Expr -> Maybe (Symbol, [Expr], Expr)
-getDCEquality senv e1 e2
+getDCEquality sEnv e1 e2
   | Just dc1 <- f1
   , Just dc2 <- f2
   = if dc1 == dc2
@@ -730,13 +728,13 @@
   | otherwise
   = Nothing
   where
-    (f1, es1) = Misc.mapFst (getDC senv) (splitEApp e1)
-    (f2, es2) = Misc.mapFst (getDC senv) (splitEApp e2)
+    (f1, es1) = Misc.mapFst (getDC sEnv) (splitEApp e1)
+    (f2, es2) = Misc.mapFst (getDC sEnv) (splitEApp e2)
 
 -- TODO: Stringy hacks
 getDC :: SymEnv -> Expr -> Maybe Symbol
-getDC senv (EVar x)
-  | isUpperSymbol x && Mb.isNothing (symEnvTheory x senv)
+getDC sEnv (EVar x)
+  | isUpperSymbol x && Mb.isNothing (symEnvTheory x sEnv)
   = Just x
 getDC _ _
   = Nothing
@@ -773,11 +771,11 @@
  -}
 
 assertSelectors :: Knowledge -> Expr -> EvalST ()
-assertSelectors γ e = do
+assertSelectors γ expr' = do
     sims <- gets (aenvSimpl . _evAEnv)
     -- cfg  <- gets evCfg
     -- _    <- foldlM (\_ s -> Vis.mapMExpr (go s) e) (mytracepp  "assertSelector" e) sims
-    forM_ sims $ \s -> Vis.mapMExpr (go s) e
+    forM_ sims $ \s -> Vis.mapMExpr (go s) expr'
   where
     go :: Rewrite -> Expr -> EvalST Expr
     go (SMeasure f dc xs bd) e@(EApp _ _)
diff --git a/src/Language/Fixpoint/Solver/Simplify.hs b/src/Language/Fixpoint/Solver/Simplify.hs
--- a/src/Language/Fixpoint/Solver/Simplify.hs
+++ b/src/Language/Fixpoint/Solver/Simplify.hs
@@ -100,9 +100,13 @@
     getOp _        = Nothing
 
     cfR :: Bop -> Double -> Double -> Maybe Expr
-    cfR bop left right = fmap go (getOp' bop)
+    cfR bop left right = go (getOp' bop)
       where
-        go f = ECon $ R $ f left right
+        go (Just f) =
+          let x = f left right
+           in if isNaN x || isInfinite x then Just $ ECon (R x)
+              else Nothing
+        go Nothing = Nothing
 
         getOp' Div      = Just (/)
         getOp' RDiv     = Just (/)
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
@@ -9,8 +9,6 @@
 {-# LANGUAGE BangPatterns          #-}
 {-# LANGUAGE RankNTypes            #-}
 
-{-# OPTIONS_GHC -Wno-name-shadowing #-}
-
 -- | This module has the functions that perform sort-checking, and related
 -- operations on Fixpoint expressions and predicates.
 
diff --git a/tests/tasty/InterpretTests.hs b/tests/tasty/InterpretTests.hs
--- a/tests/tasty/InterpretTests.hs
+++ b/tests/tasty/InterpretTests.hs
@@ -5,7 +5,7 @@
 import qualified SimplifyInterpreter
 import Test.Tasty
   ( TestTree,
-    localOption,
+    adjustOption,
     testGroup,
   )
 import Test.Tasty.QuickCheck
@@ -24,7 +24,10 @@
       [ testProperty "computes a fixpoint" (prop_fixpoint SimplifyInterpreter.interpret')
       ]
   where
-    withOptions tests' = localOption (QuickCheckMaxSize 4) (localOption (QuickCheckTests 500) tests')
+    withOptions tests' =
+      adjustOption (\(QuickCheckMaxSize n) -> QuickCheckMaxSize (div n 4)) $
+      adjustOption (\(QuickCheckTests n) -> QuickCheckTests (n * 20))
+      tests'
 
 prop_fixpoint :: (Expr -> Expr) -> Expr -> Property
 prop_fixpoint f e = f e === f (f e)