diff --git a/macaw-x86-syntax/src/Data/Macaw/X86/Symbolic/Syntax.hs b/macaw-x86-syntax/src/Data/Macaw/X86/Symbolic/Syntax.hs
index 138e67c8..57bcff04 100644
--- a/macaw-x86-syntax/src/Data/Macaw/X86/Symbolic/Syntax.hs
+++ b/macaw-x86-syntax/src/Data/Macaw/X86/Symbolic/Syntax.hs
@@ -27,6 +27,7 @@ import Data.Text qualified as Text
 import Data.Macaw.Symbolic qualified as DMS
 import Data.Macaw.X86 qualified as X86
 import Data.Macaw.X86.Symbolic qualified as X86
+import Data.Macaw.X86.Symbolic.Regs qualified as X86R
 import Data.Parameterized.Context qualified as Ctx
 import Data.Parameterized.Some (Some(..))
 import Lang.Crucible.CFG.Expr as Expr
@@ -93,23 +94,23 @@ parseReg =
   LCSM.describe "an x86_64 register" $ do
     name <- LCSC.atomName
     case name of
-      LCSA.AtomName "rip" -> pure (Some X86.rip)
-      LCSA.AtomName "rax" -> pure (Some X86.rax)
-      LCSA.AtomName "rbx" -> pure (Some X86.rbx)
-      LCSA.AtomName "rcx" -> pure (Some X86.rcx)
-      LCSA.AtomName "rdx" -> pure (Some X86.rdx)
-      LCSA.AtomName "rsp" -> pure (Some X86.rsp)
-      LCSA.AtomName "rbp" -> pure (Some X86.rbp)
-      LCSA.AtomName "rsi" -> pure (Some X86.rsi)
-      LCSA.AtomName "rdi" -> pure (Some X86.rdi)
-      LCSA.AtomName "r8" -> pure (Some X86.r8)
-      LCSA.AtomName "r9" -> pure (Some X86.r9)
-      LCSA.AtomName "r10" -> pure (Some X86.r10)
-      LCSA.AtomName "r11" -> pure (Some X86.r11)
-      LCSA.AtomName "r12" -> pure (Some X86.r12)
-      LCSA.AtomName "r13" -> pure (Some X86.r13)
-      LCSA.AtomName "r14" -> pure (Some X86.r14)
-      LCSA.AtomName "r15" -> pure (Some X86.r15)
+      LCSA.AtomName "rip" -> pure (Some X86R.rip)
+      LCSA.AtomName "rax" -> pure (Some X86R.rax)
+      LCSA.AtomName "rbx" -> pure (Some X86R.rbx)
+      LCSA.AtomName "rcx" -> pure (Some X86R.rcx)
+      LCSA.AtomName "rdx" -> pure (Some X86R.rdx)
+      LCSA.AtomName "rsp" -> pure (Some X86R.rsp)
+      LCSA.AtomName "rbp" -> pure (Some X86R.rbp)
+      LCSA.AtomName "rsi" -> pure (Some X86R.rsi)
+      LCSA.AtomName "rdi" -> pure (Some X86R.rdi)
+      LCSA.AtomName "r8" -> pure (Some X86R.r8)
+      LCSA.AtomName "r9" -> pure (Some X86R.r9)
+      LCSA.AtomName "r10" -> pure (Some X86R.r10)
+      LCSA.AtomName "r11" -> pure (Some X86R.r11)
+      LCSA.AtomName "r12" -> pure (Some X86R.r12)
+      LCSA.AtomName "r13" -> pure (Some X86R.r13)
+      LCSA.AtomName "r14" -> pure (Some X86R.r14)
+      LCSA.AtomName "r15" -> pure (Some X86R.r15)
       LCSA.AtomName _ -> empty
 
 x86AtomParser ::
diff --git a/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs b/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
index 36dd8491..d2dd185d 100644
--- a/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
+++ b/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
@@ -27,14 +27,6 @@ module Data.Macaw.X86.Symbolic
   , RegAssign
   , getReg
   , IP, GP, Flag, X87Status, X87Top, X87Tag, FPReg, YMM
-  , Rip, Rax, Rcx, Rdx, Rbx, Rsp, Rbp, Rsi, Rdi
-  , R8, R9, R10, R11, R12, R13, R14, R15
-  , CF, PF, AF, ZF, SF, TF, IF, DF, OF
-  , IE, DE, ZE, OE, UE, PE, EF, ES, C0, C1, C2, C3
-  , rip, rax, rbx, rcx, rdx, rsp, rbp, rsi, rdi
-  , r8, r9, r10, r11, r12, r13, r14, r15
-  , cf, pf, af, zf, sf, tf, if_, df, of_
-  , ie, de, ze, oe, ue, pe, ef, es, c0, c1, c2, c3
   ) where
 
 import           Control.Monad ( void )
diff --git a/x86_symbolic/src/Data/Macaw/X86/Symbolic/ABI/SysV.hs b/x86_symbolic/src/Data/Macaw/X86/Symbolic/ABI/SysV.hs
index 4e766939..02403f95 100644
--- a/x86_symbolic/src/Data/Macaw/X86/Symbolic/ABI/SysV.hs
+++ b/x86_symbolic/src/Data/Macaw/X86/Symbolic/ABI/SysV.hs
@@ -81,7 +81,7 @@ import Data.Coerce (coerce)
 import Data.Macaw.Symbolic qualified as MS
 import Data.Macaw.Symbolic.Stack qualified as MSS
 import Data.Macaw.X86 qualified as X86
-import Data.Macaw.X86.Symbolic qualified as X86S
+import Data.Macaw.X86.Symbolic.Regs qualified as X86SR
 import Data.Parameterized.Classes (ixF')
 import Data.Parameterized.Context qualified as Ctx
 import Data.Sequence qualified as Seq
@@ -109,8 +109,8 @@ stackPointerReg ::
     (StackPointer sym)
 stackPointerReg =
   Lens.lens
-    (\regs -> StackPointer (C.unRV (regs Lens.^. ixF' X86S.rsp)))
-    (\regs v -> regs Lens.& ixF' X86S.rsp Lens..~ C.RV (getStackPointer v))
+    (\regs -> StackPointer (C.unRV (regs Lens.^. ixF' X86SR.rsp)))
+    (\regs v -> regs Lens.& ixF' X86SR.rsp Lens..~ C.RV (getStackPointer v))
 
 -- | A return address
 newtype RetAddr sym = RetAddr { getRetAddr :: MM.LLVMPtr sym 64 }
diff --git a/x86_symbolic/src/Data/Macaw/X86/Symbolic/Regs.hs b/x86_symbolic/src/Data/Macaw/X86/Symbolic/Regs.hs
index adb4954e..e21eda33 100644
--- a/x86_symbolic/src/Data/Macaw/X86/Symbolic/Regs.hs
+++ b/x86_symbolic/src/Data/Macaw/X86/Symbolic/Regs.hs
@@ -1,3 +1,12 @@
+{-|
+Copyright        : (c) Galois, Inc 2024
+Maintainer       : Langston Barrett <langston@galois.com>
+
+x86_64 registers.
+
+This module is meant to be imported qualified, as it exports many terse names.
+-}
+
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
diff --git a/x86_symbolic/tests/Main.hs b/x86_symbolic/tests/Main.hs
index 169d9cc4..9f3e9e35 100644
--- a/x86_symbolic/tests/Main.hs
+++ b/x86_symbolic/tests/Main.hs
@@ -38,6 +38,7 @@ import qualified Data.Macaw.Symbolic.Testing as MST
 import qualified Data.Macaw.X86 as MX
 import           Data.Macaw.X86.Symbolic ()
 import qualified Data.Macaw.X86.Symbolic as MXS
+import qualified Data.Macaw.X86.Symbolic.Regs as MXSR
 import qualified Data.Macaw.X86.Symbolic.ABI.SysV as SysV
 import qualified What4.Config as WC
 import qualified What4.Expr.Builder as W4
@@ -103,44 +104,44 @@ main = do
   TT.defaultMainWithIngredients ingredients $
     TT.testGroup "macaw-x86-symbolic tests"
       [ TT.testGroup "Unit tests" 
-          [ TTH.testCase "ip" $ getRegName MXS.rip TTH.@?= "r!ip"
-          , TTH.testCase "rax" $ getRegName MXS.rax TTH.@?= "r!rax"
-          , TTH.testCase "rbx" $ getRegName MXS.rbx TTH.@?= "r!rbx"
-          , TTH.testCase "rcx" $ getRegName MXS.rcx TTH.@?= "r!rcx"
-          , TTH.testCase "rdx" $ getRegName MXS.rdx TTH.@?= "r!rdx"
-          , TTH.testCase "rsp" $ getRegName MXS.rsp TTH.@?= "r!rsp"
-          , TTH.testCase "rbp" $ getRegName MXS.rbp TTH.@?= "r!rbp"
-          , TTH.testCase "rsi" $ getRegName MXS.rsi TTH.@?= "r!rsi"
-          , TTH.testCase "rdi" $ getRegName MXS.rdi TTH.@?= "r!rdi"
-          , TTH.testCase "r8" $ getRegName MXS.r8 TTH.@?= "r!r8"
-          , TTH.testCase "r9" $ getRegName MXS.r9 TTH.@?= "r!r9"
-          , TTH.testCase "r10" $ getRegName MXS.r10 TTH.@?= "r!r10"
-          , TTH.testCase "r11" $ getRegName MXS.r11 TTH.@?= "r!r11"
-          , TTH.testCase "r12" $ getRegName MXS.r12 TTH.@?= "r!r12"
-          , TTH.testCase "r13" $ getRegName MXS.r13 TTH.@?= "r!r13"
-          , TTH.testCase "r14" $ getRegName MXS.r14 TTH.@?= "r!r14"
-          , TTH.testCase "r15" $ getRegName MXS.r15 TTH.@?= "r!r15"
-          , TTH.testCase "cf" $ getRegName MXS.cf TTH.@?= "r!cf"
-          , TTH.testCase "pf" $ getRegName MXS.pf TTH.@?= "r!pf"
-          , TTH.testCase "af" $ getRegName MXS.af TTH.@?= "r!af"
-          , TTH.testCase "zf" $ getRegName MXS.zf TTH.@?= "r!zf"
-          , TTH.testCase "sf" $ getRegName MXS.sf TTH.@?= "r!sf"
-          , TTH.testCase "tf" $ getRegName MXS.tf TTH.@?= "r!tf"
-          , TTH.testCase "if" $ getRegName MXS.if_ TTH.@?= "r!if"
-          , TTH.testCase "df" $ getRegName MXS.df TTH.@?= "r!df"
-          , TTH.testCase "of" $ getRegName MXS.of_ TTH.@?= "r!of"
-          , TTH.testCase "ie" $ getRegName MXS.ie TTH.@?= "r!ie"
-          , TTH.testCase "de" $ getRegName MXS.de TTH.@?= "r!de"
-          , TTH.testCase "ze" $ getRegName MXS.ze TTH.@?= "r!ze"
-          , TTH.testCase "oe" $ getRegName MXS.oe TTH.@?= "r!oe"
-          , TTH.testCase "ue" $ getRegName MXS.ue TTH.@?= "r!ue"
-          , TTH.testCase "pe" $ getRegName MXS.pe TTH.@?= "r!pe"
-          , TTH.testCase "ef" $ getRegName MXS.ef TTH.@?= "r!ef"
-          , TTH.testCase "es" $ getRegName MXS.es TTH.@?= "r!es"
-          , TTH.testCase "c0" $ getRegName MXS.c0 TTH.@?= "r!c0"
-          , TTH.testCase "c1" $ getRegName MXS.c1 TTH.@?= "r!c1"
-          , TTH.testCase "c2" $ getRegName MXS.c2 TTH.@?= "r!c2"
-          , TTH.testCase "c3" $ getRegName MXS.c3 TTH.@?= "r!c3"
+          [ TTH.testCase "ip" $ getRegName MXSR.rip TTH.@?= "r!ip"
+          , TTH.testCase "rax" $ getRegName MXSR.rax TTH.@?= "r!rax"
+          , TTH.testCase "rbx" $ getRegName MXSR.rbx TTH.@?= "r!rbx"
+          , TTH.testCase "rcx" $ getRegName MXSR.rcx TTH.@?= "r!rcx"
+          , TTH.testCase "rdx" $ getRegName MXSR.rdx TTH.@?= "r!rdx"
+          , TTH.testCase "rsp" $ getRegName MXSR.rsp TTH.@?= "r!rsp"
+          , TTH.testCase "rbp" $ getRegName MXSR.rbp TTH.@?= "r!rbp"
+          , TTH.testCase "rsi" $ getRegName MXSR.rsi TTH.@?= "r!rsi"
+          , TTH.testCase "rdi" $ getRegName MXSR.rdi TTH.@?= "r!rdi"
+          , TTH.testCase "r8" $ getRegName MXSR.r8 TTH.@?= "r!r8"
+          , TTH.testCase "r9" $ getRegName MXSR.r9 TTH.@?= "r!r9"
+          , TTH.testCase "r10" $ getRegName MXSR.r10 TTH.@?= "r!r10"
+          , TTH.testCase "r11" $ getRegName MXSR.r11 TTH.@?= "r!r11"
+          , TTH.testCase "r12" $ getRegName MXSR.r12 TTH.@?= "r!r12"
+          , TTH.testCase "r13" $ getRegName MXSR.r13 TTH.@?= "r!r13"
+          , TTH.testCase "r14" $ getRegName MXSR.r14 TTH.@?= "r!r14"
+          , TTH.testCase "r15" $ getRegName MXSR.r15 TTH.@?= "r!r15"
+          , TTH.testCase "cf" $ getRegName MXSR.cf TTH.@?= "r!cf"
+          , TTH.testCase "pf" $ getRegName MXSR.pf TTH.@?= "r!pf"
+          , TTH.testCase "af" $ getRegName MXSR.af TTH.@?= "r!af"
+          , TTH.testCase "zf" $ getRegName MXSR.zf TTH.@?= "r!zf"
+          , TTH.testCase "sf" $ getRegName MXSR.sf TTH.@?= "r!sf"
+          , TTH.testCase "tf" $ getRegName MXSR.tf TTH.@?= "r!tf"
+          , TTH.testCase "if" $ getRegName MXSR.if_ TTH.@?= "r!if"
+          , TTH.testCase "df" $ getRegName MXSR.df TTH.@?= "r!df"
+          , TTH.testCase "of" $ getRegName MXSR.of_ TTH.@?= "r!of"
+          , TTH.testCase "ie" $ getRegName MXSR.ie TTH.@?= "r!ie"
+          , TTH.testCase "de" $ getRegName MXSR.de TTH.@?= "r!de"
+          , TTH.testCase "ze" $ getRegName MXSR.ze TTH.@?= "r!ze"
+          , TTH.testCase "oe" $ getRegName MXSR.oe TTH.@?= "r!oe"
+          , TTH.testCase "ue" $ getRegName MXSR.ue TTH.@?= "r!ue"
+          , TTH.testCase "pe" $ getRegName MXSR.pe TTH.@?= "r!pe"
+          , TTH.testCase "ef" $ getRegName MXSR.ef TTH.@?= "r!ef"
+          , TTH.testCase "es" $ getRegName MXSR.es TTH.@?= "r!es"
+          , TTH.testCase "c0" $ getRegName MXSR.c0 TTH.@?= "r!c0"
+          , TTH.testCase "c1" $ getRegName MXSR.c1 TTH.@?= "r!c1"
+          , TTH.testCase "c2" $ getRegName MXSR.c2 TTH.@?= "r!c2"
+          , TTH.testCase "c3" $ getRegName MXSR.c3 TTH.@?= "r!c3"
           ]
       , TT.testGroup "Binary tests" $
           map (\mmPreset ->