-

diff --git a/src/Language/Fixpoint/Solver.hs b/src/Language/Fixpoint/Solver.hs
index 1eefd65..765401e 100644
--- a/src/Language/Fixpoint/Solver.hs
+++ b/src/Language/Fixpoint/Solver.hs
@@ -143,7 +143,7 @@ inParallelUsing f xs = do
 --------------------------------------------------------------------------------
 solveNative, solveNative' :: (NFData a, Fixpoint a) => Solver a
 --------------------------------------------------------------------------------
-solveNative !cfg !fi0 = (solveNative' cfg fi0)
+solveNative !cfg !fi0 = solveNative' cfg fi0
                           `catch`
                              (return . result)
 
@@ -152,33 +152,29 @@ result e = Result (Crash [] msg) mempty
   where
     msg  = showpp e
 
-solveNative' !cfg !fi0 = do
-  -- writeLoud $ "fq file in: \n" ++ render (toFixpoint cfg fi)
-  -- rnf fi0 `seq` donePhase Loud "Read Constraints"
-  -- let qs   = quals fi0
-  -- whenLoud $ print qs
-  let fi1  = fi0 { quals = remakeQual <$> quals fi0 }
-  -- whenLoud $ putStrLn $ showFix (quals fi1)
-  let si0   = {-# SCC "convertFormat" #-} convertFormat fi1
-  -- writeLoud $ "fq file after format convert: \n" ++ render (toFixpoint cfg si0)
-  -- rnf si0 `seq` donePhase Loud "Format Conversion"
-  let si1 = either die id $ {-# SCC "validate" #-} sanitize $!! si0
-  -- writeLoud $ "fq file after validate: \n" ++ render (toFixpoint cfg si1)
-  -- rnf si1 `seq` donePhase Loud "Validated Constraints"
-  graphStatistics cfg si1
-  let si2  = {-# SCC "wfcUniqify" #-} wfcUniqify $!! si1
-  let si3  = {-# SCC "renameAll" #-} renameAll $!! si2
-  rnf si3 `seq` donePhase Loud "Uniqify & Rename"
-  writeLoud $ "fq file after Uniqify & Rename:\n" ++ render (toFixpoint cfg si3)
-  let si4  = {-# SCC "defunctionalize" #-} defunctionalize cfg $!! si3
-  res <- {-# SCC "Sol.solve" #-} Sol.solve cfg $!! si4
-  -- rnf soln `seq` donePhase Loud "Solve2"
-  --let stat = resStatus res
-  saveSolution cfg res
-  -- when (save cfg) $ saveSolution cfg
-  -- writeLoud $ "\nSolution:\n"  ++ showpp (resSolution res)
-  -- colorStrLn (colorResult stat) (show stat)
-  return res
+solveNative' !cfg !fi0 = saveSolution cfg <<=<<
+  {-# SCC "Sol.solve" #-}        (Sol.solve       cfg $!!) =<<
+  {-# SCC "defunctionalize" #-}  (defunctionalize cfg $!!) <$>
+  ( "Uniqify & Rename"           `phase`          cfg $!!) =<<|
+  {-# SCC "renameAll" #-}        (renameAll           $!!) <$>
+  {-# SCC "wfcUniqify" #-}       (wfcUniqify          $!!) <$>
+--( "Validate Constraints"       `phase`          cfg $!!) =<<|
+                                 graphStatistics  cfg     <<=<
+  {-# SCC "validate" #-}         (either die id . sanitize) $!!
+--  "Format Conversion"          `phase`          cfg $!!
+  {-# SCC "convertFormat" #-}    convertFormat        $!!
+--  "Read Constraints"           `phase`          cfg $!!
+                                fi0
+
+phase phrase cfg si = do
+  donePhase Loud phrase
+  writeLoud $ "fq file after" ++ phrase ++ ":\n" ++ render (toFixpoint cfg si)
+  return si
+
+infixl 5 =<<|
+f =<<| a  = f =<< a
+f <<=<< a = a >>= f >> a
+f <<=< a  = f a >> pure a
 
 --------------------------------------------------------------------------------
 -- | Extract ExitCode from Solver Result ---------------------------------------
diff --git a/src/Language/Fixpoint/Types/Constraints.hs b/src/Language/Fixpoint/Types/Constraints.hs
index 0f8ef78..6238428 100644
--- a/src/Language/Fixpoint/Types/Constraints.hs
+++ b/src/Language/Fixpoint/Types/Constraints.hs
@@ -47,7 +47,7 @@ module Language.Fixpoint.Types.Constraints (
   , EQual (..)
   , eQual
   , qualifier
-  , mkQual, remakeQual
+  , mkQual
 
   -- * Results
   , FixSolution
@@ -337,9 +337,6 @@ envSort l lEnv tEnv x i
     ai  = {- trace msg $ -} fObj $ Loc l l $ tempSymbol "LHTV" i
     -- msg = "unknown symbol in qualifier: " ++ show x
 
-remakeQual :: Qualifier -> Qualifier
-remakeQual q = {- traceShow msg $ -} mkQual (qName q) (qParams q) (qBody q) (qPos q)
-
 mkQual :: Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier
 mkQual n xts p = Q n ((v, t) : yts) (subst su p)
   where