diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal
--- a/liquidhaskell.cabal
+++ b/liquidhaskell.cabal
@@ -1,5 +1,5 @@
 Name:                liquidhaskell
-Version:             0.8.2.3
+Version:             0.8.2.4
 Copyright:           2010-17 Ranjit Jhala & Niki Vazou & Eric L. Seidel, University of California, San Diego.
 Synopsis:            Liquid Types for Haskell
 Description:         Liquid Types for Haskell.
@@ -234,7 +234,7 @@
                     Language.Haskell.Liquid.Desugar.MatchLit,
                     Language.Haskell.Liquid.Desugar.DsMonad,
                     Language.Haskell.Liquid.Desugar.StaticPtrTable,
-                    Language.Haskell.Liquid.Desugar.TmOracle
+                    Language.Haskell.Liquid.Desugar.TmOracle,
                     Paths_liquidhaskell,
 
                     -- FIXME: These shouldn't really be exposed, but the linker complains otherwise...
diff --git a/src/Language/Haskell/Liquid/Bare/Check.hs b/src/Language/Haskell/Liquid/Bare/Check.hs
--- a/src/Language/Haskell/Liquid/Bare/Check.hs
+++ b/src/Language/Haskell/Liquid/Bare/Check.hs
@@ -402,7 +402,7 @@
 checkReft                    :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar (UReft r)))
                              => SEnv SortedReft -> TCEmb TyCon -> Maybe (RRType (UReft r)) -> UReft r -> Maybe Doc
 checkReft _   _   Nothing _  = Nothing -- TODO:RPropP/Ref case, not sure how to check these yet.
-checkReft env emb (Just t) _ = (\z -> dr $+$ z {- $+$ text "In environment" $+$ nest 4 (pprint env) -}) <$> checkSortedReftFull env r
+checkReft env emb (Just t) _ = (\z -> dr $+$ z) <$> checkSortedReftFull env r
   where
     r                        = rTypeSortedReft emb t
     dr                       = text "Sort Error in Refinement:" <+> pprint r
diff --git a/tests/import/lib/Bools.hs b/tests/import/lib/Bools.hs
deleted file mode 100644
--- a/tests/import/lib/Bools.hs
+++ /dev/null
@@ -1,16 +0,0 @@
-{-@ LIQUID "--exact-data-con" @-}
-
-module Bools where 
-
-{-@ measure amTrue @-}
-amTrue :: Bool -> Bool
-amTrue True = True 
-amTrue False = False 
-
-{-@ reflect boo @-}
-boo :: Bool -> Bool
-boo True = True 
-boo False = False 
-
-data Bow = Pow Int
-
diff --git a/tests/pos/ExactGADT8a.hs b/tests/pos/ExactGADT8a.hs
deleted file mode 100644
--- a/tests/pos/ExactGADT8a.hs
+++ /dev/null
@@ -1,24 +0,0 @@
-{-@ LIQUID "--exact-data-con" @-}
-
-{-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}
-
-module ExactGADT8a where
-
-{- data EntityField typ where
-            BlobXVal :: EntityField {v:_ | True }
-          | BlobYVal :: EntityField {v:_ | True }
- @-}
-data EntityField typ where
-  BlobXVal :: EntityField Int
-  BlobYVal :: EntityField Int
-
-  -- TH-GEN
-  -- data EntityField Blob typ
-  --  = typ ~ Int => BlobXVal |
-  --    typ ~ Int => BlobYVal
-
-{-@ reflect evalQBlob @-}
-evalQBlob :: EntityField a -> Bool 
-evalQBlob BlobXVal = True 
-evalQBlob BlobYVal = False 
-
diff --git a/tests/pos/ExactGADT9a.hs b/tests/pos/ExactGADT9a.hs
deleted file mode 100644
--- a/tests/pos/ExactGADT9a.hs
+++ /dev/null
@@ -1,13 +0,0 @@
-{-@ LIQUID "--exact-data-con" @-}
-
-{-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}
-
-module ExactGADT9a where
-
-import ExactGADT8a
-
-{-@ reflect zoo @-}
-zoo :: EntityField a -> Bool 
-zoo BlobXVal = True 
-zoo BlobYVal = False 
-
diff --git a/tests/pos/coerce1.hs b/tests/pos/coerce1.hs
deleted file mode 100644
--- a/tests/pos/coerce1.hs
+++ /dev/null
@@ -1,17 +0,0 @@
-
-{-@ LIQUID "--exact-data-con" @-} 
-{-# LANGUAGE GADTs #-}
-
-module Foo where 
-
-data Foo a where 
-  FInt :: Foo Int 
-  FBool :: Foo Bool
-
-f :: Foo Int -> Int 
-f z = 10 
-
-bar :: Foo a -> Int 
-bar z = case z of FInt -> f z
-                  FBool -> 10 
-
diff --git a/tests/pos/maps2.hs b/tests/pos/maps2.hs
deleted file mode 100644
--- a/tests/pos/maps2.hs
+++ /dev/null
@@ -1,41 +0,0 @@
-module Maps where
-
-
-{-@ prop0 :: x:_ -> y:{_ | y == x} -> TT @-}
-prop0 x y = (a == b)
-  where
-    a     = get x emp  
-    b     = get y emp 
-
-{-@ prop1 :: x:_ -> y:{_ | y /= x} -> TT @-}
-prop1 x y = (z == 10)
-  where
-    m1    = put x 10 emp  
-    m2    = put y 20 m1
-    z     = get x m2
-
-{-@ prop2 :: x:_ -> y:{_ | y == x} -> TT @-}
-prop2 x y = (z == 20)
-  where
-    m1    = put x 10 emp 
-    m2    = put y 20 m1
-    z     = get x m2
-
------------------------------------------------------------------------
-
-data Map k v = M
-
-{-@ embed Map as Map_t @-}
-{-@ measure Map_select :: Map k v -> k -> v @-}
-{-@ measure Map_store  :: Map k v -> k -> v -> Map k v @-}
-
-emp :: Map Int Int
-emp = undefined   
-     
-{-@ get :: k:k -> m:Map k v -> {v:v | v = Map_select m k} @-}
-get :: k -> Map k v -> v
-get = undefined 
-
-{-@ put :: k:k -> v:v -> m:Map k v -> {n:Map k v | n = Map_store m k v} @-}
-put :: k -> v -> Map k v -> Map k v
-put = undefined 
diff --git a/tests/test.hs b/tests/test.hs
--- a/tests/test.hs
+++ b/tests/test.hs
@@ -151,7 +151,6 @@
   , errorTest "tests/errors/HoleCrash1.hs"          2 "Illegal type specification for `ListDemo.t`"
   , errorTest "tests/errors/HoleCrash2.hs"          2 "Malformed application of type alias `Geq`"
   , errorTest "tests/errors/HoleCrash3.hs"          2 "Specified type does not refine Haskell type for `ListDemo.countUp`"
-  , errorTest "tests/errors/HoleCrash3.hs"          2 "Specified type does not refine Haskell type for `ListDemo.countUp`"
   , errorTest "tests/errors/BadPredApp.hs"          2 "Malformed predicate application"
   , errorTest "tests/errors/LocalHole.hs"           2 "Illegal type specification for `go`"
   , errorTest "tests/errors/UnboundAbsRef.hs"       2 "Cannot apply unbound abstract refinement `p`"