add missing wrapping step for SimpCheck

GaloisInc · May 14, 2024 · fa98b01 · fa98b01
1 parent a8ecc54
commit fa98b01
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/Pate/Verification/Simplify.hs b/src/Pate/Verification/Simplify.hs
@@ -159,7 +159,9 @@ getSimpCheck :: EquivM sym arch (WEH.SimpCheck sym (EquivM_ sym arch))
 getSimpCheck = do
   shouldCheck <- CMR.asks (PC.cfgCheckSimplifier . envConfig)
   case shouldCheck of
-    True -> return tracedSimpCheck
+    True -> withSym $ \sym -> do
+      cache_def_simp <- W4B.newIdxCache
+      return $ WEH.wrapSimpSolverCheck (WEH.unfoldDefinedFns sym (Just cache_def_simp)) tracedSimpCheck
     False -> return WEH.noSimpCheck