diff --git a/deps/saw-core b/deps/saw-core
index 40da8772ca..943f03ce02 160000
--- a/deps/saw-core
+++ b/deps/saw-core
@@ -1 +1 @@
-Subproject commit 40da8772ca86cee7c762ac0e5847ba5e78d8fff4
+Subproject commit 943f03ce02c72c834d7c0b14a9d4476125cf433e
diff --git a/deps/saw-core-coq b/deps/saw-core-coq
index 7978fdc139..f970f9763c 160000
--- a/deps/saw-core-coq
+++ b/deps/saw-core-coq
@@ -1 +1 @@
-Subproject commit 7978fdc13901045f6758b66061120ce6e1a6417e
+Subproject commit f970f9763cbb942a93d388b4fa5a7cf6044bbff3
diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index 21dfc9a3d5..9bd08a499a 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -115,7 +115,7 @@ import qualified Cryptol.Backend.Monad as C (runEval)
 import qualified Cryptol.Eval.Type as C (evalType)
 import qualified Cryptol.Eval.Value as C (fromVBit, fromVWord)
 import qualified Cryptol.Eval.Concrete as C (Concrete(..), bvVal)
-import qualified Cryptol.Utils.Ident as C (packIdent, packModName)
+import qualified Cryptol.Utils.Ident as C (mkIdent, packModName)
 import qualified Cryptol.Utils.RecordMap as C (recordFromFields)
 import Cryptol.Utils.PP (pretty)
 
@@ -192,7 +192,7 @@ readSBV path unintlst =
           SBV.TFun t1 t2 -> C.tFun (toCType t1) (toCType t2)
           SBV.TVec n t   -> C.tSeq (C.tNum n) (toCType t)
           SBV.TTuple ts  -> C.tTuple (map toCType ts)
-          SBV.TRecord bs -> C.tRec (C.recordFromFields [ (C.packIdent n, toCType t) | (n, t) <- bs ])
+          SBV.TRecord bs -> C.tRec (C.recordFromFields [ (C.mkIdent n, toCType t) | (n, t) <- bs ])
 
 
 
diff --git a/src/SAWScript/SBVParser.hs b/src/SAWScript/SBVParser.hs
index fe809d4a72..8176011aa9 100644
--- a/src/SAWScript/SBVParser.hs
+++ b/src/SAWScript/SBVParser.hs
@@ -24,6 +24,7 @@ import Control.Monad.State hiding (mapM)
 import Data.List (intercalate)
 import Data.Map (Map)
 import qualified Data.Map as Map
+import qualified Data.Text as Text
 import Data.Traversable (mapM)
 import Numeric.Natural (Natural)
 
@@ -210,7 +211,7 @@ data Typ
   | TFun Typ Typ
   | TVec SBV.Size Typ
   | TTuple [Typ]
-  | TRecord [(String, Typ)]
+  | TRecord [(FieldName, Typ)]
 
 instance Show Typ where
   show TBool = "."
@@ -218,7 +219,7 @@ instance Show Typ where
   show (TVec size t) = "[" ++ show size ++ "]" ++ show t
   show (TTuple ts) = "(" ++ intercalate "," (map show ts) ++ ")"
   show (TRecord fields) = "{" ++ intercalate "," (map showField fields) ++ "}"
-    where showField (s, t) = s ++ ":" ++ show t
+    where showField (s, t) = Text.unpack s ++ ":" ++ show t
 
 parseIRType :: SBV.IRType -> Typ
 parseIRType (SBV.TApp "." []) = TBool
@@ -227,7 +228,7 @@ parseIRType (SBV.TApp ":" [SBV.TInt n, a]) = TVec n (parseIRType a)
 parseIRType (SBV.TApp c ts)
   | c == "(" ++ replicate (length ts - 1) ',' ++ ")" = TTuple (map parseIRType ts)
 parseIRType (SBV.TRecord fields) =
-    TRecord [ (name, parseIRType t) | (name, SBV.Scheme [] [] [] t) <- fields ]
+    TRecord [ (Text.pack name, parseIRType t) | (name, SBV.Scheme [] [] [] t) <- fields ]
 parseIRType t = error ("parseIRType: " ++ show t)
 
 typSizes :: Typ -> [SBV.Size]