Apply simplification step before printing out final equivalence condi…

…tions

src/Pate/Verification/Simplify.hs

@@ -17,6 +17,7 @@ module Pate.Verification.Simplify (
   , applySimplifier
   , runSimplifier
   , getSimplifier
+  , deepPredicateSimplifier
   ) where
 
 import           Control.Monad (foldM)
@@ -218,6 +219,17 @@ applySimplifier simplifier v = withSym $ \sym -> do
     True -> withTracing @"debug_tree" "Simplifier" $ PEM.mapExpr sym (runSimplifier simplifier) v
     False -> withNoTracing $ PEM.mapExpr sym (runSimplifier simplifier) v
 
+deepPredicateSimplifier :: forall sym arch. EquivM sym arch (Simplifier sym arch)
+deepPredicateSimplifier = withSym $ \sym -> do
+  Simplifier f <- getSimplifier
+  return $ Simplifier $ \e0 ->  do
+    e1 <- liftIO $ WEH.stripAnnotations sym e0
+    e2 <- f e1
+    e4 <- case W4.exprType e0 of
+      W4.BaseBoolRepr -> simplifyPred_deep e2
+      _ -> return e2
+    applyCurrentAsms e4
+
 getSimplifier :: forall sym arch. EquivM sym arch (Simplifier sym arch)
 getSimplifier = withSym $ \sym -> do
   heuristicTimeout <- CMR.asks (PC.cfgHeuristicTimeout . envConfig)

src/Pate/Verification/StrongestPosts.hs

@@ -854,12 +854,15 @@ showFinalResult pg = withTracing @"final_result" () $ withSym $ \sym -> do
       subTrace (GraphNode nd) $ 
         emitTrace @"observable_result" (CE.ObservableCheckCounterexample report)
   subTree @"node" "Assumed Equivalence Conditions" $ do
+    simplifier <- lift $ PSi.deepPredicateSimplifier
     forM_ (getAllNodes pg) $ \nd -> do
        case getCondition pg nd ConditionEquiv of
-        Just{} -> subTrace nd $ do
+        Just cond_spec -> subTrace nd $ do
           _ <- withFreshScope (graphNodeBlocks nd) $ \scope -> do
-            -- 'withConditionsAssumed' emits the expected tracing info here
-            _ <- withGraphNode scope nd pg $ \_ _ -> return pg
+            (_,cond) <- IO.liftIO $ PS.bindSpec sym (PS.scopeVarsPair scope) cond_spec
+            cond_simplified <- PSi.applySimplifier simplifier cond
+            let pg' = setCondition nd ConditionEquiv PropagateNone (PS.mkSimSpec scope cond_simplified) pg
+            _ <- withGraphNode scope nd pg' $ \_ _ -> return pg
             return $ (Const ())
           return ()
         Nothing -> return ()

src/Pate/Verification/Widening.hs

@@ -441,16 +441,12 @@ addRefinementChoice nd gr0 = withTracing @"message" "Modify Proof Node" $ do
                   emitTrace @"message" (conditionName condK ++ " Discharged")
                   return Nothing
                 False -> do
-                  simplifier <- PSi.getSimplifier
+                  simplifier <- PSi.deepPredicateSimplifier
                   curAsm <- currentAsm
                   emitTrace @"assumption" curAsm
-                  eqCond_pred1 <- liftIO $ WEH.stripAnnotations sym eqCond_pred          
-                  eqCond_pred2 <- PSi.applySimplifier simplifier eqCond_pred1
-                  eqCond_pred3 <- PSi.simplifyPred_deep eqCond_pred2
-                  eqCond_pred4 <- applyCurrentAsms eqCond_pred3
-
-                  emitTraceLabel @"expr" (ExprLabel $ "Simplified " ++ conditionName condK) (Some eqCond_pred4)
-                  return $ Just eqCond_pred4
+                  eqCond_pred_simp <- PSi.applySimplifier simplifier eqCond_pred
+                  emitTraceLabel @"expr" (ExprLabel $ "Simplified " ++ conditionName condK) (Some eqCond_pred_simp)
+                  return $ Just eqCond_pred_simp
               case meqCond_pred' of
                 Nothing -> return $ dropCondition nd condK gr0_
                 Just eqCond_pred' -> do