diff --git a/src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs b/src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs index 35224f00..54f9a132 100644 --- a/src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs +++ b/src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs @@ -2151,9 +2151,10 @@ instance (SupportedPrim t) => Eq (Term t) where if threadId a == threadId b then identity a == identity b else unsafePerformIO $ do - a' <- fullReconstructTerm a - b' <- fullReconstructTerm b - return $ identity a' == identity b' + tid <- myWeakThreadId + a' <- toCurThreadImpl tid a + b' <- toCurThreadImpl tid b + return $ a' == b' instance (SupportedPrim t) => Hashable (Term t) where hashWithSalt s t = hashWithSalt s $ baseHash t diff --git a/test/Grisette/SymPrim/Prim/ConcurrentTests.hs b/test/Grisette/SymPrim/Prim/ConcurrentTests.hs index 7e8398bd..38dafd50 100644 --- a/test/Grisette/SymPrim/Prim/ConcurrentTests.hs +++ b/test/Grisette/SymPrim/Prim/ConcurrentTests.hs @@ -8,7 +8,7 @@ import Control.DeepSeq (force) import Control.Exception (evaluate) import Data.Hashable (Hashable (hash)) import Data.String (IsString (fromString)) -import Grisette (SymInteger (SymInteger)) +import Grisette (SymEq ((.==)), SymInteger (SymInteger), evalSymToCon, solve, z3) import Test.Framework (Test, testGroup) import Test.Framework.Providers.HUnit (testCase) import Test.HUnit ((@?=)) @@ -31,5 +31,22 @@ concurrentTests = putMVar bref p br <- takeMVar bref ar @?= br - hash ar @?= hash br + hash ar @?= hash br, + testCase "Eval" $ do + aref <- newEmptyMVar + bref <- newEmptyMVar + _ <- forkIO $ do + a <- evaluate $ force ("a" :: SymInteger) + putMVar aref a + _ <- forkIO $ do + b <- evaluate $ force ("b" :: SymInteger) + putMVar bref b + a@(SymInteger ta) <- takeMVar aref + b@(SymInteger tb) <- takeMVar bref + r <- solve z3 $ a .== b + print ta + print tb + case r of + Left err -> error $ show err + Right m -> evalSymToCon m a @?= (evalSymToCon m b :: Integer) ]