🐛 Trying to fix CI build failure that cannot be reproduced locally

src/Grisette/Internal/Backend/Solving.hs

@@ -844,7 +844,7 @@ parseModel ::
   SBVI.SMTModel ->
   SymBiMap ->
   PM.Model
-parseModel _ (SBVI.SMTModel _ _ assoc origFuncs) mp =
+parseModel _ model@(SBVI.SMTModel _ _ assoc origFuncs) mp =
   case preprocessUIFuncs origFuncs of
     Just funcs -> foldr goSingle emptyModel $ funcs ++ assocFuncs
     _ -> error "SBV Failed to parse model"
@@ -858,4 +858,7 @@ parseModel _ (SBVI.SMTModel _ _ assoc origFuncs) mp =
       Nothing ->
         error $
           "BUG: Please send a bug report. The model is not consistent with the "
-            <> "list of symbols that have been defined."
+            <> "list of symbols that have been defined. The map is "
+            <> show mp
+            <> ". The model is "
+            <> show model

src/Grisette/Internal/Backend/SymBiMap.hs

@@ -57,6 +57,16 @@ data SymBiMap = SymBiMap
     quantifiedSymbolNum :: Int
   }
 
+instance Show SymBiMap where
+  show (SymBiMap t s f _) =
+    "SymBiMap { size: "
+      ++ show s
+      ++ ", toSBV: "
+      ++ show (M.keys t)
+      ++ ", fromSBV: "
+      ++ show (M.toList f)
+      ++ " }"
+
 -- | Information about a quantified symbol.
 newtype QuantifiedSymbolInfo = QuantifiedSymbolInfo Int
   deriving (Generic, Ord, Eq, Show, Hashable, Lift, NFData)

src/Grisette/Internal/SymPrim/Prim/Internal/Caches.hs

@@ -33,7 +33,6 @@ where
 import Control.Concurrent
   ( MVar,
     ThreadId,
-    mkWeakThreadId,
     myThreadId,
     newMVar,
     putMVar,
@@ -55,10 +54,11 @@ import GHC.Weak (Weak, deRefWeak)
 import Grisette.Internal.SymPrim.Prim.Internal.Utils
   ( WeakThreadId,
     WeakThreadIdRef,
+    mkWeakThreadIdRefWithFinalizer,
     myWeakThreadId,
     weakThreadId,
   )
-import System.Mem.Weak (addFinalizer, mkWeakPtr)
+import System.Mem.Weak (mkWeakPtr)
 import Unsafe.Coerce (unsafeCoerce)
 
 -- | A unique identifier for a term.
@@ -144,8 +144,11 @@ typeMemoizedCache tid = do
           return r1
     Nothing -> do
       r1 <- mkCache
-      wtidRef <- mkWeakThreadId tid
-      addFinalizer tid $ atomicModifyIORefCAS_ termCacheCell $ HM.delete wtid
+      wtidRef <-
+        mkWeakThreadIdRefWithFinalizer tid $
+          print ("finalize", wtid)
+            >> atomicModifyIORefCAS_ termCacheCell (HM.delete wtid)
+            >> print ("finalize0", wtid)
       r <- newIORef $ HM.singleton (typeRep (Proxy @a)) (unsafeCoerce r1)
       atomicModifyIORefCAS termCacheCell $
         \m -> (HM.insert wtid (wtidRef, r) m, r1)

src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs

@@ -88,6 +88,7 @@ module Grisette.Internal.SymPrim.Prim.Internal.Term
     FPRoundingBinaryOp (..),
     FloatingUnaryOp (..),
     Term (..),
+    toCurThread,
     identity,
     typeHashId,
     introSupportedPrimConstraint,
@@ -2151,9 +2152,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
@@ -3497,6 +3499,12 @@ toCurThreadImpl tid t | termThreadId t == tid = return t
 toCurThreadImpl _ t = fullReconstructTerm t
 {-# INLINE toCurThreadImpl #-}
 
+toCurThread :: forall t. Term t -> IO (Term t)
+toCurThread t = do
+  tid <- myWeakThreadId
+  toCurThreadImpl tid t
+{-# INLINE toCurThread #-}
+
 -- | Construct and internalizing a 'ConTerm'.
 curThreadConTerm :: (SupportedPrim t) => t -> IO (Term t)
 curThreadConTerm t = intern $ UConTerm t

src/Grisette/Internal/SymPrim/Prim/Internal/Utils.hs

@@ -7,6 +7,7 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE UnboxedTuples #-}
 {-# LANGUAGE UnliftedFFITypes #-}
 {-# LANGUAGE ViewPatterns #-}
 
@@ -30,25 +31,27 @@ module Grisette.Internal.SymPrim.Prim.Internal.Utils
     WeakThreadIdRef,
     myWeakThreadId,
     weakThreadRefAlive,
+    mkWeakThreadIdRefWithFinalizer,
   )
 where
 
 #if MIN_VERSION_base(4,19,0)
 import GHC.Conc.Sync
-  ( ThreadId,
+  ( ThreadId(ThreadId),
     ThreadStatus (ThreadDied, ThreadFinished),
     fromThreadId,
     myThreadId,
     threadStatus,
   )
+import GHC.Exts (mkWeak#)
 #else
 import GHC.Conc
   ( ThreadId (ThreadId),
     ThreadStatus (ThreadDied, ThreadFinished),
     myThreadId,
     threadStatus,
   )
-import GHC.Exts (Addr#, ThreadId#, unsafeCoerce#)
+import GHC.Exts (Addr#, ThreadId#, unsafeCoerce#, mkWeak#)
 #if __GLASGOW_HASKELL__ >= 904
 #elif __GLASGOW_HASKELL__ >= 900
 import Foreign.C.Types (CLong (CLong))
@@ -58,7 +61,9 @@ import Foreign.C.Types (CInt (CInt))
 #endif
 import Data.Typeable (cast)
 import Data.Word (Word64)
-import System.Mem.Weak (Weak, deRefWeak)
+import GHC.IO (IO (IO))
+import GHC.Weak (Weak (Weak))
+import System.Mem.Weak (deRefWeak)
 import Type.Reflection
   ( TypeRep,
     Typeable,
@@ -158,3 +163,8 @@ weakThreadRefAlive wtid = do
       st <- threadStatus tid
       return $ st `notElem` [ThreadFinished, ThreadDied]
 {-# INLINE weakThreadRefAlive #-}
+
+mkWeakThreadIdRefWithFinalizer :: ThreadId -> IO () -> IO (Weak ThreadId)
+mkWeakThreadIdRefWithFinalizer t@(ThreadId t#) (IO finalizer) = IO $ \s ->
+  case mkWeak# t# t finalizer s of
+    (# s1, w #) -> (# s1, Weak w #)

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)
     ]

test/Main.hs

@@ -77,7 +77,7 @@ import Grisette.Unified.UnifiedConstructorTest (unifiedConstructorTest)
 import Test.Framework (Test, defaultMain, testGroup)
 
 main :: IO ()
-main = do
+main =
   defaultMain
     [ coreTests,
       irTests,