diff --git a/macaw-x86-syntax/LICENSE b/macaw-x86-syntax/LICENSE
new file mode 100644
index 00000000..511de500
--- /dev/null
+++ b/macaw-x86-syntax/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2024 Galois Inc.
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+  * Redistributions of source code must retain the above copyright
+    notice, this list of conditions and the following disclaimer.
+
+  * Redistributions in binary form must reproduce the above copyright
+    notice, this list of conditions and the following disclaimer in
+    the documentation and/or other materials provided with the
+    distribution.
+
+  * Neither the name of Galois, Inc. nor the names of its contributors
+    may be used to endorse or promote products derived from this
+    software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/macaw-x86-syntax/README.md b/macaw-x86-syntax/README.md
new file mode 100644
index 00000000..445ecfa7
--- /dev/null
+++ b/macaw-x86-syntax/README.md
@@ -0,0 +1,36 @@
+# macaw-x86-syntax
+
+This package provides concrete syntax for macaw-x86-symbolic types and
+operations.
+
+Concretely, it implements a `ParserHooks` for use with [`crucible-syntax`][syn].
+This `ParserHooks` supports the following types and operations:
+
+**Types**:
+
+- `X86Regs`: the struct of all x86_64 registers
+
+**Operations**:
+
+- `get-reg :: X86Reg -> X86Regs -> t`: extract an x86 register
+- `set-reg :: X86Reg -> t -> X86Regs -> X86Regs`: set an x86 register
+- Registers:
+  - `rip :: X86Reg`: instruction pointer
+  - `rax :: X86Reg`: SysV return value register
+  - `rbx :: X86Reg`: general-purpose register
+  - `rcx :: X86Reg`: general-purpose register
+  - `rdx :: X86Reg`: general-purpose register
+  - `rsp :: X86Reg`: stack pointer
+  - `rbp :: X86Reg`: base pointer
+  - `rsi :: X86Reg`: general-purpose register
+  - `rdi :: X86Reg`: general-purpose register
+  - `r8 :: X86Reg`: general-purpose register
+  - `r9 :: X86Reg`: general-purpose register
+  - `r10 :: X86Reg`: general-purpose register
+  - `r11 :: X86Reg`: general-purpose register
+  - `r12 :: X86Reg`: general-purpose register
+  - `r13 :: X86Reg`: general-purpose register
+  - `r14 :: X86Reg`: general-purpose register
+  - `r15 :: X86Reg`: general-purpose register
+
+[syn]: https://github.com/GaloisInc/crucible/tree/master/crucible-syntax
diff --git a/macaw-x86-syntax/macaw-x86-syntax.cabal b/macaw-x86-syntax/macaw-x86-syntax.cabal
new file mode 100644
index 00000000..a0d61362
--- /dev/null
+++ b/macaw-x86-syntax/macaw-x86-syntax.cabal
@@ -0,0 +1,133 @@
+Cabal-version: 2.2
+Name:          macaw-x86-syntax
+Version:       0.1
+Author:        Galois Inc.
+Maintainer:    langston@galois.com
+Build-type:    Simple
+License:       BSD-3-Clause
+License-file:  LICENSE
+Category:      Language
+Synopsis:      A syntax for macaw-x86-symbolic control-flow graphs
+-- Description:
+
+extra-doc-files: README.md
+extra-source-files:
+  test-data/*.cbl
+  test-data/*.out.good
+
+common shared
+  -- Specifying -Wall and -Werror can cause the project to fail to build on
+  -- newer versions of GHC simply due to new warnings being added to -Wall. To
+  -- prevent this from happening we manually list which warnings should be
+  -- considered errors. We also list some warnings that are not in -Wall, though
+  -- try to avoid "opinionated" warnings (though this judgement is clearly
+  -- subjective).
+  --
+  -- Warnings are grouped by the GHC version that introduced them, and then
+  -- alphabetically.
+  --
+  -- A list of warnings and the GHC version in which they were introduced is
+  -- available here:
+  -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html
+
+  -- Since GHC 8.10 or earlier:
+  ghc-options:
+    -Wall
+    -Werror=compat-unqualified-imports
+    -Werror=deferred-type-errors
+    -Werror=deprecated-flags
+    -Werror=deprecations
+    -Werror=deriving-defaults
+    -Werror=dodgy-foreign-imports
+    -Werror=duplicate-exports
+    -Werror=empty-enumerations
+    -Werror=identities
+    -Werror=inaccessible-code
+    -Werror=incomplete-patterns
+    -Werror=incomplete-record-updates
+    -Werror=incomplete-uni-patterns
+    -Werror=inline-rule-shadowing
+    -Werror=missed-extra-shared-lib
+    -Werror=missing-exported-signatures
+    -Werror=missing-fields
+    -Werror=missing-home-modules
+    -Werror=missing-methods
+    -Werror=overflowed-literals
+    -Werror=overlapping-patterns
+    -Werror=partial-fields
+    -Werror=partial-type-signatures
+    -Werror=simplifiable-class-constraints
+    -Werror=star-binder
+    -Werror=star-is-type
+    -Werror=tabs
+    -Werror=typed-holes
+    -Werror=unrecognised-pragmas
+    -Werror=unrecognised-warning-flags
+    -Werror=unsupported-calling-conventions
+    -Werror=unsupported-llvm-version
+    -Werror=unticked-promoted-constructors
+    -Werror=unused-imports
+    -Werror=warnings-deprecations
+    -Werror=wrong-do-bind
+
+  if impl(ghc >= 9.2)
+    ghc-options:
+      -Werror=ambiguous-fields
+      -Werror=operator-whitespace
+      -Werror=operator-whitespace-ext-conflict
+      -Werror=redundant-bang-patterns
+
+  if impl(ghc >= 9.4)
+    ghc-options:
+      -Werror=forall-identifier
+      -Werror=misplaced-pragmas
+      -Werror=redundant-strictness-flags
+      -Werror=type-equality-out-of-scope
+      -Werror=type-equality-requires-operators
+
+  ghc-prof-options: -O2 -fprof-auto-top
+  default-language: Haskell2010
+
+library
+  import: shared
+
+  build-depends:
+    base >= 4.13,
+    containers,
+    crucible,
+    crucible-syntax,
+    macaw-base,
+    macaw-symbolic,
+    macaw-x86,
+    macaw-x86-symbolic,
+    mtl,
+    parameterized-utils,
+    text,
+    what4,
+
+  hs-source-dirs: src
+
+  exposed-modules:
+    Data.Macaw.X86.Symbolic.Syntax
+
+test-suite macaw-x86-syntax-tests
+  import: shared
+  type: exitcode-stdio-1.0
+  main-is: Test.hs
+  hs-source-dirs: test
+  build-depends:
+    base,
+    containers,
+    crucible >= 0.1,
+    crucible-syntax,
+    crucible-llvm-syntax,
+    filepath,
+    macaw-symbolic,
+    macaw-symbolic-syntax,
+    macaw-x86,
+    macaw-x86-symbolic,
+    macaw-x86-syntax,
+    parameterized-utils >= 0.1.7,
+    tasty,
+    tasty-golden,
+    text,
diff --git a/macaw-x86-syntax/src/Data/Macaw/X86/Symbolic/Syntax.hs b/macaw-x86-syntax/src/Data/Macaw/X86/Symbolic/Syntax.hs
new file mode 100644
index 00000000..138e67c8
--- /dev/null
+++ b/macaw-x86-syntax/src/Data/Macaw/X86/Symbolic/Syntax.hs
@@ -0,0 +1,140 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+-- | 'LCSC.ParserHooks' for parsing macaw-x86-symbolic CFGs.
+module Data.Macaw.X86.Symbolic.Syntax
+  ( x86ParserHooks
+    -- * Types
+  , x86TypeParser
+    -- * Operations
+  , parseRegs
+  , parseReg
+  , x86AtomParser
+  ) where
+
+import Control.Applicative ( empty )
+import Control.Monad qualified as Monad
+import Control.Monad.IO.Class (MonadIO)
+import Control.Monad.State.Strict (MonadState)
+import Control.Monad.Writer.Strict (MonadWriter)
+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.Parameterized.Context qualified as Ctx
+import Data.Parameterized.Some (Some(..))
+import Lang.Crucible.CFG.Expr as Expr
+import Lang.Crucible.CFG.Reg (Atom, Stmt)
+import Lang.Crucible.CFG.Reg qualified as Reg
+import Lang.Crucible.Syntax.Atoms qualified as LCSA
+import Lang.Crucible.Syntax.Concrete qualified as LCSC
+import Lang.Crucible.Syntax.Monad qualified as LCSM
+import Lang.Crucible.Types qualified as LCT
+import What4.ProgramLoc (Posd(..))
+
+-- | Parser hooks for macaw-x86-symbolic CFGs
+x86ParserHooks :: LCSC.ParserHooks ext
+x86ParserHooks =
+  LCSC.ParserHooks
+  { LCSC.extensionTypeParser = x86TypeParser
+  , LCSC.extensionParser = x86AtomParser
+  }
+
+---------------------------------------------------------------------
+-- Types
+
+-- Helper, not exported
+namedAtom :: LCSM.MonadSyntax LCSA.Atomic m => Text.Text -> m ()
+namedAtom expectName = do
+  name <- LCSC.atomName
+  Monad.unless (name == LCSA.AtomName expectName) LCSM.cut
+
+-- Helper, not exported
+x86RegTypes :: Ctx.Assignment LCT.TypeRepr (DMS.MacawCrucibleRegTypes X86.X86_64)
+x86RegTypes = DMS.crucArchRegTypes X86.x86_64MacawSymbolicFns
+
+-- Helper, not exported
+x86RegStructType :: LCT.TypeRepr (DMS.ArchRegStruct X86.X86_64)
+x86RegStructType = LCT.StructRepr x86RegTypes
+
+-- | Parser for type extensions to Crucible syntax
+x86TypeParser ::
+  LCSM.MonadSyntax LCSA.Atomic m =>
+  m (Some LCT.TypeRepr)
+x86TypeParser = do
+  namedAtom "X86Regs"
+  pure (Some x86RegStructType)
+
+---------------------------------------------------------------------
+-- Operations
+
+parseRegs ::
+  ( LCSM.MonadSyntax LCSA.Atomic m
+  , MonadIO m
+  , MonadState (LCSC.SyntaxState s) m
+  , MonadWriter [Posd (Stmt ext s)] m
+  , IsSyntaxExtension ext
+  , ?parserHooks :: LCSC.ParserHooks ext
+  ) =>
+  m (Atom s (DMS.ArchRegStruct X86.X86_64))
+parseRegs =
+  LCSM.describe "a struct of x86_64 register values" $ do
+    assign <- LCSC.operands (Ctx.Empty Ctx.:> x86RegStructType)
+    pure (assign Ctx.! Ctx.baseIndex)
+
+parseReg :: LCSM.MonadSyntax LCSA.Atomic m => m (Some (Ctx.Index (DMS.MacawCrucibleRegTypes X86.X86_64)))
+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 _ -> empty
+
+x86AtomParser ::
+  ( LCSM.MonadSyntax LCSA.Atomic m
+  , MonadIO m
+  , MonadState (LCSC.SyntaxState s) m
+  , MonadWriter [Posd (Stmt ext s)] m
+  , IsSyntaxExtension ext
+  , ?parserHooks :: LCSC.ParserHooks ext
+  ) =>
+  m (Some (Atom s))
+x86AtomParser =
+  LCSM.depCons LCSC.atomName $
+    \case
+      LCSA.AtomName "get-reg" -> do
+        loc <- LCSM.position
+        (Some reg, regs) <- LCSM.cons parseReg parseRegs
+        let regTy = x86RegTypes Ctx.! reg
+        Some <$> LCSC.freshAtom loc (Reg.EvalApp (Expr.GetStruct regs reg regTy))
+      LCSA.AtomName "set-reg" -> do
+        loc <- LCSM.position
+        LCSM.depCons parseReg $ \(Some reg) -> do
+          let regTy = x86RegTypes Ctx.! reg
+          assign <- LCSC.operands (Ctx.Empty Ctx.:> regTy Ctx.:> x86RegStructType)
+          let (rest, regs) = Ctx.decompose assign
+          let (Ctx.Empty, val) = Ctx.decompose rest
+          Some <$> LCSC.freshAtom loc (Reg.EvalApp (Expr.SetStruct x86RegTypes regs reg val))
+      LCSA.AtomName _ -> empty
diff --git a/macaw-x86-syntax/test-data/.gitignore b/macaw-x86-syntax/test-data/.gitignore
new file mode 100644
index 00000000..f47cb204
--- /dev/null
+++ b/macaw-x86-syntax/test-data/.gitignore
@@ -0,0 +1 @@
+*.out
diff --git a/macaw-x86-syntax/test-data/get-regs.cbl b/macaw-x86-syntax/test-data/get-regs.cbl
new file mode 100644
index 00000000..083c35f9
--- /dev/null
+++ b/macaw-x86-syntax/test-data/get-regs.cbl
@@ -0,0 +1,37 @@
+(defun @id ((regs X86Regs)) X86Regs
+  (start start:
+    (let vrip (get-reg rip regs))
+    (let vrax (get-reg rax regs))
+    (let vrbx (get-reg rbx regs))
+    (let vrcx (get-reg rcx regs))
+    (let vrdx (get-reg rdx regs))
+    (let vrsp (get-reg rsp regs))
+    (let vrbp (get-reg rbp regs))
+    (let vrsi (get-reg rsi regs))
+    (let vrdi (get-reg rdi regs))
+    (let vr8 (get-reg r8 regs))
+    (let vr9 (get-reg r9 regs))
+    (let vr10 (get-reg r10 regs))
+    (let vr11 (get-reg r11 regs))
+    (let vr12 (get-reg r12 regs))
+    (let vr13 (get-reg r13 regs))
+    (let vr14 (get-reg r14 regs))
+    (let vr15 (get-reg r15 regs))
+    (let regs0 (set-reg rip vrip regs))
+    (let regs1 (set-reg rax vrax regs0))
+    (let regs2 (set-reg rbx vrbx regs1))
+    (let regs3 (set-reg rcx vrcx regs2))
+    (let regs4 (set-reg rdx vrdx regs3))
+    (let regs5 (set-reg rsp vrsp regs4))
+    (let regs6 (set-reg rbp vrbp regs5))
+    (let regs7 (set-reg rsi vrsi regs6))
+    (let regs8 (set-reg rdi vrdi regs7))
+    (let regs9 (set-reg r8 vr8 regs8))
+    (let regs10 (set-reg r9 vr9 regs9))
+    (let regs11 (set-reg r10 vr10 regs10))
+    (let regs12 (set-reg r11 vr11 regs11))
+    (let regs13 (set-reg r12 vr12 regs12))
+    (let regs14 (set-reg r13 vr13 regs13))
+    (let regs15 (set-reg r14 vr14 regs14))
+    (let regs16 (set-reg r15 vr15 regs15))
+    (return regs16)))
\ No newline at end of file
diff --git a/macaw-x86-syntax/test-data/get-regs.out.good b/macaw-x86-syntax/test-data/get-regs.out.good
new file mode 100644
index 00000000..060d1f06
--- /dev/null
+++ b/macaw-x86-syntax/test-data/get-regs.out.good
@@ -0,0 +1,111 @@
+(defun @id ((regs X86Regs)) X86Regs
+   (start start:
+      (let vrip (get-reg rip regs))
+      (let vrax (get-reg rax regs))
+      (let vrbx (get-reg rbx regs))
+      (let vrcx (get-reg rcx regs))
+      (let vrdx (get-reg rdx regs))
+      (let vrsp (get-reg rsp regs))
+      (let vrbp (get-reg rbp regs))
+      (let vrsi (get-reg rsi regs))
+      (let vrdi (get-reg rdi regs))
+      (let vr8 (get-reg r8 regs))
+      (let vr9 (get-reg r9 regs))
+      (let vr10 (get-reg r10 regs))
+      (let vr11 (get-reg r11 regs))
+      (let vr12 (get-reg r12 regs))
+      (let vr13 (get-reg r13 regs))
+      (let vr14 (get-reg r14 regs))
+      (let vr15 (get-reg r15 regs))
+      (let regs0 (set-reg rip vrip regs))
+      (let regs1 (set-reg rax vrax regs0))
+      (let regs2 (set-reg rbx vrbx regs1))
+      (let regs3 (set-reg rcx vrcx regs2))
+      (let regs4 (set-reg rdx vrdx regs3))
+      (let regs5 (set-reg rsp vrsp regs4))
+      (let regs6 (set-reg rbp vrbp regs5))
+      (let regs7 (set-reg rsi vrsi regs6))
+      (let regs8 (set-reg rdi vrdi regs7))
+      (let regs9 (set-reg r8 vr8 regs8))
+      (let regs10 (set-reg r9 vr9 regs9))
+      (let regs11 (set-reg r10 vr10 regs10))
+      (let regs12 (set-reg r11 vr11 regs11))
+      (let regs13 (set-reg r12 vr12 regs12))
+      (let regs14 (set-reg r13 vr13 regs13))
+      (let regs15 (set-reg r14 vr14 regs14))
+      (let regs16 (set-reg r15 vr15 regs15))
+      (return regs16)))
+
+id
+%0
+  % 3:15
+  $1 = getStruct($0, 0, IntrinsicRepr LLVM_pointer [BVRepr 64])
+  % 4:15
+  $2 = getStruct($0, 1, IntrinsicRepr LLVM_pointer [BVRepr 64])
+  % 5:15
+  $3 = getStruct($0, 4, IntrinsicRepr LLVM_pointer [BVRepr 64])
+  % 6:15
+  $4 = getStruct($0, 2, IntrinsicRepr LLVM_pointer [BVRepr 64])
+  % 7:15
+  $5 = getStruct($0, 3, IntrinsicRepr LLVM_pointer [BVRepr 64])
+  % 8:15
+  $6 = getStruct($0, 5, IntrinsicRepr LLVM_pointer [BVRepr 64])
+  % 9:15
+  $7 = getStruct($0, 6, IntrinsicRepr LLVM_pointer [BVRepr 64])
+  % 10:15
+  $8 = getStruct($0, 7, IntrinsicRepr LLVM_pointer [BVRepr 64])
+  % 11:15
+  $9 = getStruct($0, 8, IntrinsicRepr LLVM_pointer [BVRepr 64])
+  % 12:14
+  $10 = getStruct($0, 9, IntrinsicRepr LLVM_pointer [BVRepr 64])
+  % 13:14
+  $11 = getStruct($0, 10, IntrinsicRepr LLVM_pointer [BVRepr 64])
+  % 14:15
+  $12 = getStruct($0, 11, IntrinsicRepr LLVM_pointer [BVRepr 64])
+  % 15:15
+  $13 = getStruct($0, 12, IntrinsicRepr LLVM_pointer [BVRepr 64])
+  % 16:15
+  $14 = getStruct($0, 13, IntrinsicRepr LLVM_pointer [BVRepr 64])
+  % 17:15
+  $15 = getStruct($0, 14, IntrinsicRepr LLVM_pointer [BVRepr 64])
+  % 18:15
+  $16 = getStruct($0, 15, IntrinsicRepr LLVM_pointer [BVRepr 64])
+  % 19:15
+  $17 = getStruct($0, 16, IntrinsicRepr LLVM_pointer [BVRepr 64])
+  % 20:16
+  $18 = setStruct([IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, IntrinsicRepr LLVM_pointer [BVRepr 3], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512]], $0, 0, $1)
+  % 21:16
+  $19 = setStruct([IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, IntrinsicRepr LLVM_pointer [BVRepr 3], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512]], $18, 1, $2)
+  % 22:16
+  $20 = setStruct([IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, IntrinsicRepr LLVM_pointer [BVRepr 3], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512]], $19, 4, $3)
+  % 23:16
+  $21 = setStruct([IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, IntrinsicRepr LLVM_pointer [BVRepr 3], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512]], $20, 2, $4)
+  % 24:16
+  $22 = setStruct([IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, IntrinsicRepr LLVM_pointer [BVRepr 3], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512]], $21, 3, $5)
+  % 25:16
+  $23 = setStruct([IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, IntrinsicRepr LLVM_pointer [BVRepr 3], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512]], $22, 5, $6)
+  % 26:16
+  $24 = setStruct([IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, IntrinsicRepr LLVM_pointer [BVRepr 3], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512]], $23, 6, $7)
+  % 27:16
+  $25 = setStruct([IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, IntrinsicRepr LLVM_pointer [BVRepr 3], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512]], $24, 7, $8)
+  % 28:16
+  $26 = setStruct([IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, IntrinsicRepr LLVM_pointer [BVRepr 3], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512]], $25, 8, $9)
+  % 29:16
+  $27 = setStruct([IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, IntrinsicRepr LLVM_pointer [BVRepr 3], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512]], $26, 9, $10)
+  % 30:17
+  $28 = setStruct([IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, IntrinsicRepr LLVM_pointer [BVRepr 3], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512]], $27, 10, $11)
+  % 31:17
+  $29 = setStruct([IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, IntrinsicRepr LLVM_pointer [BVRepr 3], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512]], $28, 11, $12)
+  % 32:17
+  $30 = setStruct([IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, IntrinsicRepr LLVM_pointer [BVRepr 3], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512]], $29, 12, $13)
+  % 33:17
+  $31 = setStruct([IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, IntrinsicRepr LLVM_pointer [BVRepr 3], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512]], $30, 13, $14)
+  % 34:17
+  $32 = setStruct([IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, IntrinsicRepr LLVM_pointer [BVRepr 3], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512]], $31, 14, $15)
+  % 35:17
+  $33 = setStruct([IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, IntrinsicRepr LLVM_pointer [BVRepr 3], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512]], $32, 15, $16)
+  % 36:17
+  $34 = setStruct([IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], IntrinsicRepr LLVM_pointer [BVRepr 64], BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, BoolRepr, IntrinsicRepr LLVM_pointer [BVRepr 3], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 2], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 80], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512], IntrinsicRepr LLVM_pointer [BVRepr 512]], $33, 16, $17)
+  % 37:5
+  return $34
+  % no postdom
diff --git a/macaw-x86-syntax/test-data/get-rip.cbl b/macaw-x86-syntax/test-data/get-rip.cbl
new file mode 100644
index 00000000..7d2f0fc4
--- /dev/null
+++ b/macaw-x86-syntax/test-data/get-rip.cbl
@@ -0,0 +1,4 @@
+(defun @id ((regs X86Regs)) (Ptr 64)
+  (start start:
+    (let b (get-reg rip regs))
+    (return b)))
\ No newline at end of file
diff --git a/macaw-x86-syntax/test-data/get-rip.out.good b/macaw-x86-syntax/test-data/get-rip.out.good
new file mode 100644
index 00000000..e7e8a3d3
--- /dev/null
+++ b/macaw-x86-syntax/test-data/get-rip.out.good
@@ -0,0 +1,10 @@
+(defun @id ((regs X86Regs)) (Ptr 64)
+   (start start: (let b (get-reg rip regs)) (return b)))
+
+id
+%0
+  % 3:12
+  $1 = getStruct($0, 0, IntrinsicRepr LLVM_pointer [BVRepr 64])
+  % 4:5
+  return $1
+  % no postdom
diff --git a/macaw-x86-syntax/test-data/regs.cbl b/macaw-x86-syntax/test-data/regs.cbl
new file mode 100644
index 00000000..ebf6cf9b
--- /dev/null
+++ b/macaw-x86-syntax/test-data/regs.cbl
@@ -0,0 +1,3 @@
+(defun @id ((regs X86Regs)) X86Regs
+  (start start:
+    (return regs)))
\ No newline at end of file
diff --git a/macaw-x86-syntax/test-data/regs.out.good b/macaw-x86-syntax/test-data/regs.out.good
new file mode 100644
index 00000000..14e7a19e
--- /dev/null
+++ b/macaw-x86-syntax/test-data/regs.out.good
@@ -0,0 +1,8 @@
+(defun @id ((regs X86Regs)) X86Regs
+   (start start: (return regs)))
+
+id
+%0
+  % 3:5
+  return $0
+  % no postdom
diff --git a/macaw-x86-syntax/test/Test.hs b/macaw-x86-syntax/test/Test.hs
new file mode 100644
index 00000000..83f57b15
--- /dev/null
+++ b/macaw-x86-syntax/test/Test.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Main (main) where
+
+import Data.List (sort)
+import Data.Proxy (Proxy(Proxy))
+import Data.Text.IO qualified as T
+import System.FilePath
+import System.IO
+
+import Test.Tasty (defaultMain, TestTree, testGroup)
+import Test.Tasty.Golden
+
+import Lang.Crucible.Syntax.Prog (doParseCheck)
+
+import Data.Macaw.Symbolic.Syntax (machineCodeParserHooks)
+
+import Data.Macaw.X86 (X86_64)
+import Data.Macaw.X86.Symbolic ()  -- TraversableFC instance for (MacawExt X86) statements and expressions
+import Data.Macaw.X86.Symbolic.Syntax (x86ParserHooks)
+
+main :: IO ()
+main = do
+  parseTests <- findTests "Parse tests" "test-data" testParser
+  defaultMain $ testGroup "Tests" [parseTests]
+
+findTests :: String -> FilePath -> (FilePath -> FilePath -> IO ()) -> IO TestTree
+findTests groupName testDir testAction =
+  do inputs <- findByExtension [".cbl"] testDir
+     return $ testGroup groupName
+       [ goldenFileTestCase input testAction
+       | input <- sort inputs
+       ]
+
+goldenFileTestCase :: FilePath -> (FilePath -> FilePath -> IO ()) -> TestTree
+goldenFileTestCase input testAction =
+  goldenVsFileDiff
+   (takeBaseName input) -- test name
+   (\x y -> ["diff", "-u", x, y])
+   goodFile -- golden file path
+   outFile
+   (testAction input outFile) -- action whose result is tested
+  where
+    outFile = replaceExtension input ".out"
+    goodFile = replaceExtension input ".out.good"
+
+testParser :: FilePath -> FilePath -> IO ()
+testParser inFile outFile =
+  do contents <- T.readFile inFile
+     let ?parserHooks = machineCodeParserHooks (Proxy @X86_64) x86ParserHooks
+     withFile outFile WriteMode $ doParseCheck inFile contents True
+
diff --git a/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs b/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
index 104ace92..b36fc71b 100644
--- a/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
+++ b/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
@@ -1,18 +1,17 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE TypeSynonymInstances #-}
-{-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Data.Macaw.X86.Symbolic
   ( x86_64MacawSymbolicFns
@@ -20,11 +19,29 @@ module Data.Macaw.X86.Symbolic
   , SymFuns(..), newSymFuns
   , X86StmtExtension(..)
 
+  , x86RegAssignment
   , lookupX86Reg
   , updateX86Reg
   , freshX86Reg
 
   , RegAssign
+  , rip
+  , rax
+  , rbx
+  , rcx
+  , rdx
+  , rsp
+  , rbp
+  , rsi
+  , rdi
+  , r8
+  , r9
+  , r10
+  , r11
+  , r12
+  , r13
+  , r14
+  , r15
   , getReg
   , IP, GP, Flag, X87Status, X87Top, X87Tag, FPReg, YMM
   ) where
@@ -104,13 +121,68 @@ type X87Tag n    = 39 + n   -- 8
 type FPReg n     = 47 + n   -- 8
 type YMM n       = 55 + n   -- 16
 
+-- The following definitions are tightly coupled to that of ArchRegContext for
+-- X86_64. Unit tests in the test suite ensure that they are consistent with
+-- x86RegAssignment (below).
+
+rip :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
+rip = Ctx.extendIndex (Ctx.nextIndex (knownSize @_ @(CtxRepeat 0 (MM.LLVMPointerType 64))))
+
+rax :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
+rax = Ctx.extendIndex (Ctx.nextIndex (knownSize @_ @(CtxRepeat 1 (MM.LLVMPointerType 64))))
+
+rcx :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
+rcx = Ctx.extendIndex (Ctx.nextIndex (knownSize @_ @(CtxRepeat 2 (MM.LLVMPointerType 64))))
+
+rdx :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
+rdx = Ctx.extendIndex (Ctx.nextIndex (knownSize @_ @(CtxRepeat 3 (MM.LLVMPointerType 64))))
+
+rbx :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
+rbx = Ctx.extendIndex (Ctx.nextIndex (knownSize @_ @(CtxRepeat 4 (MM.LLVMPointerType 64))))
+
+rsp :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
+rsp = Ctx.extendIndex (Ctx.nextIndex (knownSize @_ @(CtxRepeat 5 (MM.LLVMPointerType 64))))
+
+rbp :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
+rbp = Ctx.extendIndex (Ctx.nextIndex (knownSize @_ @(CtxRepeat 6 (MM.LLVMPointerType 64))))
+
+rsi :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
+rsi = Ctx.extendIndex (Ctx.nextIndex (knownSize @_ @(CtxRepeat 7 (MM.LLVMPointerType 64))))
+
+rdi :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
+rdi = Ctx.extendIndex (Ctx.nextIndex (knownSize @_ @(CtxRepeat 8 (MM.LLVMPointerType 64))))
+
+r8 :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
+r8 = Ctx.extendIndex (Ctx.nextIndex (knownSize @_ @(CtxRepeat 9 (MM.LLVMPointerType 64))))
+
+r9 :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
+r9 = Ctx.extendIndex (Ctx.nextIndex (knownSize @_ @(CtxRepeat 10 (MM.LLVMPointerType 64))))
+
+r10 :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
+r10 = Ctx.extendIndex (Ctx.nextIndex (knownSize @_ @(CtxRepeat 11 (MM.LLVMPointerType 64))))
+
+r11 :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
+r11 = Ctx.extendIndex (Ctx.nextIndex (knownSize @_ @(CtxRepeat 12 (MM.LLVMPointerType 64))))
+
+r12 :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
+r12 = Ctx.extendIndex (Ctx.nextIndex (knownSize @_ @(CtxRepeat 13 (MM.LLVMPointerType 64))))
+
+r13 :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
+r13 = Ctx.extendIndex (Ctx.nextIndex (knownSize @_ @(CtxRepeat 14 (MM.LLVMPointerType 64))))
+
+r14 :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
+r14 = Ctx.extendIndex (Ctx.nextIndex (knownSize @_ @(CtxRepeat 15 (MM.LLVMPointerType 64))))
+
+r15 :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) (MM.LLVMPointerType 64)
+r15 = Ctx.extendIndex (Ctx.nextIndex (knownSize @_ @(CtxRepeat 16 (MM.LLVMPointerType 64))))
+
 getReg ::
   forall n t f. (Idx n (ArchRegContext M.X86_64) t) => RegAssign f -> f t
 getReg x = x ^. (field @n)
 
 x86RegName' :: M.X86Reg tp -> String
 x86RegName' M.X86_IP     = "ip"
-x86RegName' (M.X86_GP r) = show $ F.reg64No r
+x86RegName' (M.X86_GP r) = show r
 x86RegName' (M.X86_FlagReg r) = show r
 x86RegName' (M.X87_StatusReg r) = show r
 x86RegName' M.X87_TopReg = "x87Top"
@@ -124,7 +196,7 @@ x86RegName r = C.systemSymbol $ "r!" ++ x86RegName' r
 gpReg :: Int -> M.X86Reg (M.BVType 64)
 gpReg = M.X86_GP . F.Reg64 . fromIntegral
 
--- | The x86 flag registers that are directly supported by Macw.
+-- | The x86 flag registers that are directly supported by Macaw.
 flagRegs :: Assignment M.X86Reg (CtxRepeat 9 M.BoolType)
 flagRegs =
   Empty :> M.CF :> M.PF :> M.AF :> M.ZF :> M.SF :> M.TF :> M.IF :> M.DF :> M.OF
diff --git a/x86_symbolic/tests/Main.hs b/x86_symbolic/tests/Main.hs
index 8e75d383..a165b3f1 100644
--- a/x86_symbolic/tests/Main.hs
+++ b/x86_symbolic/tests/Main.hs
@@ -33,6 +33,7 @@ import qualified Data.Macaw.Symbolic as MS
 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 What4.Config as WC
 import qualified What4.Interface as WI
 import qualified What4.ProblemFeatures as WPF
@@ -45,6 +46,7 @@ import qualified Lang.Crucible.LLVM.MemModel as LLVM
 
 import qualified What4.FloatMode as W4
 import qualified What4.Expr.Builder as W4
+import qualified Data.Parameterized.Context as Ctx
 
 -- | A Tasty option to tell us to save SMT queries and responses to /tmp for debugging purposes
 data SaveSMT = SaveSMT Bool
@@ -70,6 +72,17 @@ ingredients = TT.includingOptions [ TTO.Option (Proxy @SaveSMT)
                                   , TTO.Option (Proxy @SaveMacaw)
                                   ] : TT.defaultIngredients
 
+getRegName ::
+  Ctx.Index (MS.MacawCrucibleRegTypes MX.X86_64) t ->
+  String
+getRegName reg =
+  case Ctx.intIndex (Ctx.indexVal reg) (Ctx.size MXS.x86RegAssignment) of
+    Just (Some i) ->
+      let r = MXS.x86RegAssignment Ctx.! i
+          rName = MS.crucGenArchRegName MXS.x86_64MacawSymbolicFns r
+      in show rName
+    Nothing -> error "impossible"
+
 main :: IO ()
 main = do
   -- These are pass/fail in that the assertions in the "pass" set are true (and
@@ -82,11 +95,32 @@ main = do
   let passTests mmPreset = TT.testGroup "True assertions" (map (mkSymExTest passRes mmPreset) passTestFilePaths)
   let failTests mmPreset = TT.testGroup "False assertions" (map (mkSymExTest failRes mmPreset) failTestFilePaths)
   TT.defaultMainWithIngredients ingredients $
-    TT.testGroup "Binary Tests" $
-    map (\mmPreset ->
-          TT.testGroup (MST.describeMemModelPreset mmPreset)
-                       [passTests mmPreset, failTests mmPreset])
-        [MST.DefaultMemModel, MST.LazyMemModel]
+    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"
+          ]
+      , TT.testGroup "Binary tests" $
+          map (\mmPreset ->
+                TT.testGroup (MST.describeMemModelPreset mmPreset)
+                             [passTests mmPreset, failTests mmPreset])
+              [MST.DefaultMemModel, MST.LazyMemModel]
+      ]
 
 hasTestPrefix :: Some (M.DiscoveryFunInfo arch) -> Maybe (BS8.ByteString, Some (M.DiscoveryFunInfo arch))
 hasTestPrefix (Some dfi) = do