Revert "Removes sort checks for Map and Set during internalization (#2440)"

This reverts commit 4195d94.

Author: MirceaS

kore/src/Kore/Builtin.hs

@@ -198,6 +198,6 @@ internalize tools =
   where
     internalize1 =
             List.internalize tools
-        .   Map.internalize
-        .   Set.internalize
+        .   Map.internalize tools
+        .   Set.internalize tools
         .   InternalBytes.internalize

kore/src/Kore/Builtin/Map.hs

@@ -52,6 +52,7 @@ import Data.Text
 import Kore.Attribute.Hook
     ( Hook (..)
     )
+import qualified Kore.Attribute.Symbol as Attribute
 import qualified Kore.Builtin.AssociativeCommutative as Ac
 import Kore.Builtin.Attributes
     ( isConstructorModulo_
@@ -484,14 +485,18 @@ internalize subterms.
 
 internalize
     :: InternalVariable variable
-    => TermLike variable
+    => SmtMetadataTools Attribute.Symbol
+    -> TermLike variable
     -> TermLike variable
-internalize termLike
+internalize tools termLike
+  | fromMaybe False (isMapSort tools sort')
   -- Ac.toNormalized is greedy about 'normalizing' opaque terms, we should only
   -- apply it if we know the term head is a constructor-like symbol.
-  | App_ symbol _ <- termLike
+  , App_ symbol _ <- termLike
   , isConstructorModulo_ symbol = Ac.toNormalizedInternalMap termLike
   | otherwise = termLike
+  where
+    sort' = termLikeSort termLike
 
 {- | Simplify the conjunction or equality of two concrete Map domain values.
 

kore/src/Kore/Builtin/Set.hs

@@ -52,6 +52,9 @@ import qualified Data.Set as Set
 import Data.Text
     ( Text
     )
+import qualified Kore.Attribute.Symbol as Attribute
+    ( Symbol
+    )
 import qualified Kore.Builtin.AssociativeCommutative as Ac
 import Kore.Builtin.Attributes
     ( isConstructorModulo_
@@ -485,14 +488,18 @@ internalize subterms.
  -}
 internalize
     :: InternalVariable variable
-    => TermLike variable
+    => SmtMetadataTools Attribute.Symbol
+    -> TermLike variable
     -> TermLike variable
-internalize termLike
+internalize tools termLike
+  | fromMaybe False (isSetSort tools sort')
   -- Ac.toNormalized is greedy about 'normalizing' opaque terms, we should only
   -- apply it if we know the term head is a constructor-like symbol.
-  | App_ symbol _ <- termLike
+  , App_ symbol _ <- termLike
   , isConstructorModulo_ symbol = Ac.toNormalizedInternalSet termLike
   | otherwise = termLike
+  where
+    sort' = termLikeSort termLike
 
 {- | Simplify the conjunction or equality of two concrete Set domain values.