diff --git a/src/Cryptol/TypeCheck/Solve.hs b/src/Cryptol/TypeCheck/Solve.hs
index 4d5907e1..8520151c 100644
--- a/src/Cryptol/TypeCheck/Solve.hs
+++ b/src/Cryptol/TypeCheck/Solve.hs
@@ -38,6 +38,8 @@ import           Data.Set ( Set )
 import qualified Data.Set as Set
 import qualified SimpleSMT as SMT
 
+import           Text.PrettyPrint(text)
+
 -- Add additional constraints that ensure validity of type function.
 checkTypeFunction :: TFun -> [Type] -> [Prop]
 checkTypeFunction TCSub [a,b]             = [ a >== b, pFin b]
@@ -139,15 +141,36 @@ numericRight g  = case Num.exportProp (goal g) of
                     Just (p,vm)  -> Right ((g,vm), p)
                     Nothing -> Left g
 
+_testSimpGoals :: IO ()
+_testSimpGoals = Num.withSolver $ \s ->
+  do mb <- simpGoals s gs
+     case mb of
+       Just (gs1,su) ->
+          do debugBlock s "Simplified goals"
+                $ mapM_ (debugLog s . show . pp . goal) gs1
+             debugLog s (show (pp su))
+       Nothing -> debugLog s "Impossible"
+  where
+  gs = map fakeGoal [ tv 0 =#= num 5 ]
+    -- [ tv 0 =#= tInf, tMod (num 3) (tv 0) =#= num 4 ]
+
+  fakeGoal p = Goal { goalSource = undefined, goalRange = undefined, goal = p }
+  tv n = TVar (TVFree n KNum Set.empty (text "test var"))
+  num x = tNum (x :: Int)
+
 -- | Assumes that the substitution has been applied to the goals.
 simpGoals :: Num.Solver -> [Goal] -> IO (Maybe ([Goal],Subst))
 simpGoals s gs0 =
   do let (unsolvedClassCts,numCts) = solveClassCts gs0
+
          varMap = Map.unions [ vm | ((_,vm),_) <- numCts ]
          updCt prop (g,vs) = case Num.importProp varMap prop of
                                Just [g1] -> (g { goal = g1 }, vs)
-                               -- XXX: Could we get multiple gs?
-                               _         -> (g, vs)
+
+                               r -> panic "simpGoals"
+                                      [ "Unexpected import results"
+                                      , show r
+                                      ]
      case numCts of
        [] -> return $ Just (unsolvedClassCts, emptySubst)
        _  -> do mbOk <- Num.checkDefined s updCt uvs numCts
diff --git a/src/Cryptol/TypeCheck/Solver/CrySAT.hs b/src/Cryptol/TypeCheck/Solver/CrySAT.hs
index b7a4b82e..5c1391f3 100644
--- a/src/Cryptol/TypeCheck/Solver/CrySAT.hs
+++ b/src/Cryptol/TypeCheck/Solver/CrySAT.hs
@@ -65,7 +65,9 @@ checkDefined s updCt uniVars props0 = withScope s (go Map.empty [] props0)
   where
   go knownImps done notDone =
     do (newNotDone, novelDone) <- checkDefined' s updCt notDone
+       putStrLn "Checking"
        (possible,  imps)       <- check s uniVars
+       putStrLn ("Possible: " ++ show possible)
        if not possible
          then return Nothing
          else
@@ -79,6 +81,7 @@ checkDefined s updCt uniVars props0 = withScope s (go Map.empty [] props0)
                                    )
                 else
                   do mapM_ addImpProp (Map.toList novelImps)
+                     -- Apply subst to knownImps?
                      let newImps    = Map.union novelImps knownImps
                          impDone    = map (updDone novelImps) newDone
                          impNotDone = map (updNotDone novelImps) newNotDone
@@ -114,6 +117,8 @@ checkDefined' s updCt props0 =
      go False [] [] ps
 
   where
+
+
   -- Everything is defined: keep going.
   go _    isDef []       [] = return ([], isDef)
 
@@ -278,7 +283,7 @@ withSolver :: (Solver -> IO a) -> IO a
 withSolver k =
   do logger <- SMT.newLogger
      solver <- SMT.newSolver "cvc4" ["--lang=smt2", "--incremental"]
-                                                   Nothing -- (Just logger)
+                                                   Nothing --} (Just logger)
      SMT.setLogic solver "QF_LIA"
      declared <- newIORef viEmpty
      nameSource <- newIORef 0
@@ -308,7 +313,7 @@ declareVar Solver { .. } a =
           let fin_a = smtFinName a
           _  <- SMT.declare solver fin_a SMT.tBool
           SMT.assert solver (SMT.geq e (SMT.int 0))
-          SMT.assert solver (SMT.const fin_a)     -- HMM ???
+          -- SMT.assert solver (SMT.const fin_a)     -- HMM ???
           modifyIORef' declared (viInsert a)
 
 -- | Add an assertion to the current context.
@@ -352,7 +357,8 @@ check Solver { .. } uniVars =
        SMT.Unsat   -> return (False, Map.empty)
        SMT.Unknown -> return (True, Map.empty)
        SMT.Sat     ->
-         do names <- viNames `fmap` readIORef declared
+         do putStrLn "Trying improvements"
+            names <- viNames `fmap` readIORef declared
             m     <- fmap Map.fromList (mapM getVal names)
             imps  <- toSubst `fmap` cryImproveModel solver uniVars m
 
diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs b/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs
index 68bb01af..ba273d3f 100644
--- a/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs
+++ b/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs
@@ -40,7 +40,7 @@ crySimplify p = trace ("simp: " ++ show (ppProp p)) $
 
 -- | Simplify a property, if possible.
 crySimplify' :: Prop -> Prop
-crySimplify' p = fromMaybe p (crySimplifyMaybe p)
+crySimplify' p = crySimplify p -- fromMaybe p (crySimplifyMaybe p)
 
 -- | Simplify a property, if possibly.
 crySimplifyMaybe :: Prop -> Maybe Prop
@@ -346,7 +346,6 @@ cryKnownFin a isFin prop =
 
 
 
-
 -- | Negation.
 cryNot :: Prop -> Maybe Prop
 cryNot prop =