Fix unsat cache thanks to @blishko

Author: msooseth

src/EVM/SymExec.hs

@@ -5,7 +5,7 @@ module EVM.SymExec where
 
 import Control.Concurrent.Async (concurrently, mapConcurrently)
 import Control.Concurrent.Spawn (parMapIO, pool)
-import Control.Concurrent.STM (TVar, readTVarIO, newTVarIO)
+import Control.Concurrent.STM (TVar, readTVarIO, newTVarIO, writeTVar, atomically, readTVar)
 import Control.Monad (when, forM_, forM)
 import Control.Monad.IO.Unlift
 import Control.Monad.Operational qualified as Operational
@@ -856,7 +856,10 @@ equivalenceCheck' solvers branchesA branchesB create = do
     check knownUnsat props = do
       ku <- liftIO $ readTVarIO knownUnsat
       if subsetAny props ku then pure Qed
-      else fst <$> checkSatWithProps solvers (Set.toList props)
+      else do
+         (ret, _) <- checkSatWithProps solvers (Set.toList props)
+         when (ret == Qed) $ liftIO $ atomically $ readTVar knownUnsat >>= writeTVar knownUnsat . (props :)
+         pure ret
 
     -- Allows us to run the queries in parallel. Note that this (seems to) run it
     -- from left-to-right, and with a max of K threads. This is in contrast to