diff --git a/.travis.yml b/.travis.yml
index aba990a9..cf78b7de 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -33,21 +33,10 @@ install:
    fi
  - travis_retry cabal update -v
  - sed -i 's/^jobs:/-- jobs:/' ${HOME}/.cabal/config
- # - cabal install --only-dependencies --enable-tests --enable-benchmarks --dry -v > installplan.txt
- # - stack install macaw-x86 --only-dependencies --test --dry-run -v 2> installplan.txt
- # - sed -i -e '1,/^Resolving /d' installplan.txt; cat installplan.txt
 
 # Here starts the actual work to be performed for the package under test;
 # any command which exits with a non-zero exit code causes the build to fail.
 script:
  - travis_wait stack --no-terminal --skip-ghc-check setup
- - stack --stack-yaml stack.ghc-8.2.2.yaml build macaw-x86 macaw-x86-symbolic
- - stack --stack-yaml stack.ghc-8.2.2.yaml test macaw-x86
-
-# Check that the resulting source distribution can be built & installed.
-# If there are no other `.tar.gz` files in `dist`, this can be even simpler:
-# `cabal install --force-reinstalls dist/*-*.tar.gz`
-# - SRC_TGZ=$(cabal info . | awk '{print $2;exit}').tar.gz &&
-#   (cd dist && cabal install --force-reinstalls "$SRC_TGZ")
-
-# EOF
+ - stack --stack-yaml stack.ghc-8.6.3.yaml build macaw-x86 macaw-x86-symbolic
+ - stack --stack-yaml stack.ghc-8.6.3.yaml test macaw-x86
diff --git a/base/src/Data/Macaw/CFG/App.hs b/base/src/Data/Macaw/CFG/App.hs
index af0a9e16..75e72590 100644
--- a/base/src/Data/Macaw/CFG/App.hs
+++ b/base/src/Data/Macaw/CFG/App.hs
@@ -74,6 +74,10 @@ data App (f :: Type -> Kind.Type) (tp :: Type) where
   -- all @false@.
   UExt :: (1 <= m, m+1 <= n, 1 <= n) => f (BVType m) -> NatRepr n -> App f (BVType n)
 
+  -- | This casts an expression from one type to another that should
+  -- use the same number of bytes in memory.
+  Bitcast :: f tp -> TypeRepr out -> App f out
+
   ----------------------------------------------------------------------
   -- Bitvector operations
 
@@ -257,15 +261,17 @@ ppAppA :: Applicative m
       -> m Doc
 ppAppA pp a0 =
   case a0 of
+    Eq x y      -> sexprA "eq" [ pp x, pp y ]
     Mux _ c x y -> sexprA "mux" [ pp c, pp x, pp y ]
-    Trunc x w -> sexprA "trunc" [ pp x, ppNat w ]
     TupleField _ x i -> sexprA "tuple_field" [ pp x, prettyPure (P.indexValue i) ]
-    SExt x w -> sexprA "sext" [ pp x, ppNat w ]
-    UExt x w -> sexprA "uext" [ pp x, ppNat w ]
     AndApp x y -> sexprA "and" [ pp x, pp y ]
     OrApp  x y -> sexprA "or"  [ pp x, pp y ]
     NotApp x   -> sexprA "not" [ pp x ]
     XorApp  x y -> sexprA "xor"  [ pp x, pp y ]
+    Trunc x w -> sexprA "trunc" [ pp x, ppNat w ]
+    SExt x w -> sexprA "sext" [ pp x, ppNat w ]
+    UExt x w -> sexprA "uext" [ pp x, ppNat w ]
+    Bitcast x tp -> sexprA "bitcast" [ pp x, pure (text (show tp)) ]
     BVAdd _ x y   -> sexprA "bv_add" [ pp x, pp y ]
     BVAdc _ x y c -> sexprA "bv_adc" [ pp x, pp y, pp c ]
     BVSub _ x y -> sexprA "bv_sub" [ pp x, pp y ]
@@ -283,7 +289,6 @@ ppAppA pp a0 =
     BVShl _ x y -> sexprA "bv_shl" [ pp x, pp y ]
     BVShr _ x y -> sexprA "bv_shr" [ pp x, pp y ]
     BVSar _ x y -> sexprA "bv_sar" [ pp x, pp y ]
-    Eq x y      -> sexprA "eq" [ pp x, pp y ]
     PopCount _ x -> sexprA "popcount" [ pp x ]
     ReverseBytes _ x -> sexprA "reverse_bytes" [ pp x ]
     UadcOverflows x y c -> sexprA "uadc_overflows" [ pp x, pp y, pp c ]
@@ -311,6 +316,7 @@ instance HasRepr (App f) TypeRepr where
       Trunc _ w -> BVTypeRepr w
       SExt  _ w -> BVTypeRepr w
       UExt  _ w -> BVTypeRepr w
+      Bitcast _ tp -> tp
 
       AndApp{} -> knownRepr
       OrApp{}  -> knownRepr
diff --git a/base/src/Data/Macaw/Types.hs b/base/src/Data/Macaw/Types.hs
index cb8d45cc..f1e7db35 100644
--- a/base/src/Data/Macaw/Types.hs
+++ b/base/src/Data/Macaw/Types.hs
@@ -70,70 +70,8 @@ n128 = knownNat
 n256 :: NatRepr 256
 n256 = knownNat
 
-------------------------------------------------------------------------
--- Type
-
-data Type
-  = -- | A bitvector with the given number of bits.
-    BVType Nat
-    -- | A floating point in the given format.
-  | FloatType FloatInfo
-    -- | A Boolean value
-  | BoolType
-    -- | A tuple of types
-  | TupleType [Type]
-
-
--- Return number of bytes in the type.
-type family TypeBytes (tp :: Type) :: Nat where
-  TypeBytes (BVType  8) = 1
-  TypeBytes (BVType 16) = 2
-  TypeBytes (BVType 32) = 4
-  TypeBytes (BVType 64) = 8
-  TypeBytes (FloatType fi) = FloatInfoBytes fi
-
--- Return number of bits in the type.
-type family TypeBits (tp :: Type) :: Nat where
-  TypeBits (BVType n) = n
-  TypeBits (FloatType fi) = 8 * FloatInfoBytes fi
-
-type BVType = 'BVType
-
-type FloatType = 'FloatType
-
-type BoolType = 'BoolType
-
-type TupleType = 'TupleType
-
--- | A runtime representation of @Type@ for case matching purposes.
-data TypeRepr (tp :: Type) where
-  BoolTypeRepr :: TypeRepr BoolType
-  BVTypeRepr :: (1 <= n) => !(NatRepr n) -> TypeRepr (BVType n)
-  FloatTypeRepr :: !(FloatInfoRepr fi) -> TypeRepr (FloatType fi)
-  TupleTypeRepr :: !(P.List TypeRepr ctx) -> TypeRepr (TupleType ctx)
-
-type_width :: TypeRepr (BVType n) -> NatRepr n
-type_width (BVTypeRepr n) = n
-
-instance Show (TypeRepr tp) where
-  show BoolTypeRepr = "bool"
-  show (BVTypeRepr w) = "[" ++ show w ++ "]"
-  show (FloatTypeRepr fi) = show fi ++ "_float"
-  show (TupleTypeRepr P.Nil) = "()"
-  show (TupleTypeRepr (h P.:< z)) =
-    "(" ++ show h ++ foldrFC (\tp r -> "," ++ show tp ++ r) ")" z
-
-instance KnownRepr TypeRepr BoolType where
-  knownRepr = BoolTypeRepr
-
-instance (KnownNat n, 1 <= n) => KnownRepr TypeRepr (BVType n) where
-  knownRepr = BVTypeRepr knownNat
-
-instance (KnownRepr FloatInfoRepr fi) => KnownRepr TypeRepr (FloatType fi) where
-  knownRepr = FloatTypeRepr knownRepr
-
-instance (KnownRepr (P.List TypeRepr) l) => KnownRepr TypeRepr  (TupleType l) where
-  knownRepr = TupleTypeRepr knownRepr
+n512 :: NatRepr 512
+n512 = knownNat
 
 ------------------------------------------------------------------------
 -- Floating point sizes
@@ -217,18 +155,92 @@ floatInfoBitsIsPos = \case
   QuadFloatRepr   -> LeqProof
   X86_80FloatRepr -> LeqProof
 
+$(return [])
+
+------------------------------------------------------------------------
+-- Type
+
+data Type
+  = -- | A bitvector with the given number of bits.
+    BVType Nat
+    -- | A floating point in the given format.
+  | FloatType FloatInfo
+    -- | A Boolean value
+  | BoolType
+    -- | A tuple of types
+  | TupleType [Type]
+    -- | A vector of types
+  | VecType Nat Type
+
+
+-- Return number of bytes in the type.
+type family TypeBytes (tp :: Type) :: Nat where
+  TypeBytes (BVType  8) = 1
+  TypeBytes (BVType 16) = 2
+  TypeBytes (BVType 32) = 4
+  TypeBytes (BVType 64) = 8
+  TypeBytes (FloatType fi) = FloatInfoBytes fi
+  TypeBytes (VecType n tp) = n * TypeBytes tp
+
+-- Return number of bits in the type.
+type family TypeBits (tp :: Type) :: Nat where
+  TypeBits (BVType n) = n
+  TypeBits (FloatType fi) = 8 * FloatInfoBytes fi
+
+type BVType = 'BVType
+
+type FloatType = 'FloatType
+
+type BoolType = 'BoolType
+
+type TupleType = 'TupleType
+
 -- | The bitvector associated with the given floating-point format.
 type FloatBVType (fi :: FloatInfo) = BVType (FloatInfoBits fi)
 
-floatBVTypeRepr :: FloatInfoRepr fi -> TypeRepr (FloatBVType fi)
-floatBVTypeRepr fi | LeqProof <- floatInfoBitsIsPos fi =
-  BVTypeRepr $ floatInfoBits fi
+$(pure [])
 
-$(return [])
+
+-- | A runtime representation of @Type@ for case matching purposes.
+data TypeRepr (tp :: Type) where
+  BoolTypeRepr :: TypeRepr BoolType
+  BVTypeRepr :: (1 <= n) => !(NatRepr n) -> TypeRepr (BVType n)
+  FloatTypeRepr :: !(FloatInfoRepr fi) -> TypeRepr (FloatType fi)
+  TupleTypeRepr :: !(P.List TypeRepr ctx) -> TypeRepr (TupleType ctx)
+  VectorTypeRepr :: NatRepr n -> TypeRepr tp -> TypeRepr (VecType n tp)
+
+type_width :: TypeRepr (BVType n) -> NatRepr n
+type_width (BVTypeRepr n) = n
+
+instance Show (TypeRepr tp) where
+  show BoolTypeRepr = "bool"
+  show (BVTypeRepr w) = "[" ++ show w ++ "]"
+  show (FloatTypeRepr fi) = show fi ++ "_float"
+  show (TupleTypeRepr P.Nil) = "()"
+  show (TupleTypeRepr (h P.:< z)) =
+    "(" ++ show h ++ foldrFC (\tp r -> "," ++ show tp ++ r) ")" z
+  show (VectorTypeRepr c tp) = "(vec " ++ show c ++ " " ++ show tp ++ ")"
+
+instance ShowF TypeRepr
+
+instance KnownRepr TypeRepr BoolType where
+  knownRepr = BoolTypeRepr
+
+instance (KnownNat n, 1 <= n) => KnownRepr TypeRepr (BVType n) where
+  knownRepr = BVTypeRepr knownNat
+
+instance (KnownRepr FloatInfoRepr fi) => KnownRepr TypeRepr (FloatType fi) where
+  knownRepr = FloatTypeRepr knownRepr
+
+instance (KnownRepr (P.List TypeRepr) l) => KnownRepr TypeRepr  (TupleType l) where
+  knownRepr = TupleTypeRepr knownRepr
+
+$(pure [])
 
 instance TestEquality TypeRepr where
   testEquality = $(structuralTypeEquality [t|TypeRepr|]
-    [ (ConType [t|NatRepr|] `TypeApp` AnyType, [|testEquality|])
+    [ (ConType [t|NatRepr|]       `TypeApp` AnyType, [|testEquality|])
+    , (ConType [t|TypeRepr|]      `TypeApp` AnyType, [|testEquality|])
     , (ConType [t|FloatInfoRepr|] `TypeApp` AnyType, [|testEquality|])
     , ( ConType [t|P.List|] `TypeApp` AnyType `TypeApp` AnyType
       , [|testEquality|]
@@ -237,7 +249,8 @@ instance TestEquality TypeRepr where
 
 instance OrdF TypeRepr where
   compareF = $(structuralTypeOrd [t|TypeRepr|]
-    [ (ConType [t|NatRepr|] `TypeApp` AnyType, [|compareF|])
+    [ (ConType [t|NatRepr|]       `TypeApp` AnyType, [|compareF|])
+    , (ConType [t|TypeRepr|]      `TypeApp` AnyType, [|compareF|])
     , (ConType [t|FloatInfoRepr|] `TypeApp` AnyType, [|compareF|])
     , (ConType [t|P.List|] `TypeApp` AnyType `TypeApp` AnyType, [|compareF|])
     ])
@@ -247,6 +260,10 @@ instance TestEquality FloatInfoRepr where
 instance OrdF FloatInfoRepr where
   compareF = $(structuralTypeOrd [t|FloatInfoRepr|] [])
 
+floatBVTypeRepr :: FloatInfoRepr fi -> TypeRepr (FloatBVType fi)
+floatBVTypeRepr fi | LeqProof <- floatInfoBitsIsPos fi =
+  BVTypeRepr $ floatInfoBits fi
+
 ------------------------------------------------------------------------
 --
 
diff --git a/deps/flexdis86 b/deps/flexdis86
index 2ac3d616..64a3b815 160000
--- a/deps/flexdis86
+++ b/deps/flexdis86
@@ -1 +1 @@
-Subproject commit 2ac3d616996885f93b66c870520381cb09e783ca
+Subproject commit 64a3b8154a654e7079a6a5253a00d4fe8dac9934
diff --git a/stack.ghc-8.2.2.yaml b/stack.ghc-8.2.2.yaml
index 13228650..06c7f6f6 100644
--- a/stack.ghc-8.2.2.yaml
+++ b/stack.ghc-8.2.2.yaml
@@ -20,4 +20,5 @@ extra-deps:
 - monadLib-3.7.3
 - panic-0.4.0.1
 - IntervalMap-0.6.1.0
+- itanium-abi-0.1.1.0
 resolver: lts-11.22
diff --git a/stack.ghc-8.6.3.yaml b/stack.ghc-8.6.3.yaml
new file mode 100644
index 00000000..fd717282
--- /dev/null
+++ b/stack.ghc-8.6.3.yaml
@@ -0,0 +1,24 @@
+flags:
+  time-locale-compat:
+    old-locale: false
+
+packages:
+- base
+- x86
+- symbolic
+- x86_symbolic
+- deps/crucible/what4
+- deps/crucible/crucible
+- deps/crucible/crucible-llvm
+- deps/dwarf
+- deps/elf-edit
+- deps/flexdis86
+- deps/flexdis86/binary-symbols
+- deps/llvm-pretty
+- deps/parameterized-utils
+extra-deps:
+- boomerang-1.4.5.6
+- itanium-abi-0.1.1.0
+- monadLib-3.9
+- panic-0.4.0.1
+resolver: lts-13.7
diff --git a/x86/src/Data/Macaw/X86/Getters.hs b/x86/src/Data/Macaw/X86/Getters.hs
index 851f8726..f915ae6a 100644
--- a/x86/src/Data/Macaw/X86/Getters.hs
+++ b/x86/src/Data/Macaw/X86/Getters.hs
@@ -233,7 +233,8 @@ getSomeBVLocation v =
     F.XMMReg r       -> do avx <- isAVX
                            pure $ SomeBV $ if avx then xmm_avx r
                                                   else xmm_sse r
-    F.YMMReg r       -> pure $ SomeBV $ ymm r
+    F.YMMReg r       -> do avx <- isAVX
+                           pure $ SomeBV $ if avx then ymm_zero r else ymm_preserve r
     F.SegmentValue s -> pure $ SomeBV $ SegmentReg s
     F.X87Register i -> mk (X87StackRegister i)
     F.FarPointer _      -> fail "FarPointer"
@@ -319,8 +320,8 @@ getSignExtendedValue v out_w =
     F.Mem64  ar   -> mk =<< getBV64Addr ar
     F.Mem128 ar   -> mk =<< getBV128Addr ar
     F.Mem256 ar   -> mk =<< getBV256Addr ar
-    F.XMMReg r                      -> mk (xmm_avx r)
-    F.YMMReg r                      -> mk (ymm r)
+    F.XMMReg r  -> mk (xmm_avx r)
+    F.YMMReg r  -> mk (ymm_zero r)
 
     F.ByteImm  i
       | Just Refl <- testEquality n8 out_w ->
@@ -474,6 +475,6 @@ readXMMValue _ = fail "XMM Instruction given unexpected value."
 
 -- | Get a YMM value
 readYMMValue :: F.Value -> X86Generator st ids (Expr ids (BVType 256))
-readYMMValue (F.YMMReg r) = get (ymm r)
+readYMMValue (F.YMMReg r) = get (ymm_zero r)
 readYMMValue (F.Mem256 a) = readBVAddress a ymmMemRepr
 readYMMValue _ = fail "YMM Instruction given unexpected value."
diff --git a/x86/src/Data/Macaw/X86/Monad.hs b/x86/src/Data/Macaw/X86/Monad.hs
index bb7b45af..eaf05263 100644
--- a/x86/src/Data/Macaw/X86/Monad.hs
+++ b/x86/src/Data/Macaw/X86/Monad.hs
@@ -81,7 +81,8 @@ module Data.Macaw.X86.Monad
   , ax, bx, cx, dx
   , al, dl
   , ah
-  , ymm
+  , ymm_preserve
+  , ymm_zero
   , xmm_sse
   , xmm_avx
   , xmmOwner
@@ -838,17 +839,22 @@ ah = reg_high8 R.RAX
 rip :: Location addr (BVType 64)
 rip = fullRegister R.X86_IP
 
-ymm :: F.YMMReg -> Location addr (BVType 256)
-ymm = fullRegister . R.YMM . F.ymmRegNo
+-- | Access the low-order 256-bits in legacy SSE mode (upper 256-bits preserved)
+ymm_preserve :: F.YMMReg -> Location addr (BVType 256)
+ymm_preserve r = subRegister n0 n256 (R.ZMM (F.ymmRegNo r))
+
+-- | Access the low-order 256-bits in legacy SSE mode (upper 256-bits zeroed)
+ymm_zero :: F.YMMReg -> Location addr (BVType 256)
+ymm_zero r = constUpperBitsOnWriteRegister n256 ZeroExtendOnWrite (R.ZMM (F.ymmRegNo r))
 
 xmm_sse :: F.XMMReg -> Location addr (BVType 128)
-xmm_sse = reg_low128_sse . xmmOwner
+xmm_sse r = subRegister n0 n128 (R.ZMM (F.xmmRegNo r))
 
 xmm_avx :: F.XMMReg -> Location addr (BVType 128)
-xmm_avx = reg_low128_avx . xmmOwner
+xmm_avx r = constUpperBitsOnWriteRegister n128 ZeroExtendOnWrite (R.ZMM (F.xmmRegNo r))
 
-xmmOwner :: F.XMMReg -> X86Reg (BVType 256)
-xmmOwner = R.YMM . F.xmmRegNo
+xmmOwner :: F.XMMReg -> X86Reg (BVType 512)
+xmmOwner r = R.ZMM (F.xmmRegNo r)
 
 ------------------------------------------------------------------------
 
diff --git a/x86/src/Data/Macaw/X86/Semantics/AVX.hs b/x86/src/Data/Macaw/X86/Semantics/AVX.hs
index 756dd414..f78df92c 100644
--- a/x86/src/Data/Macaw/X86/Semantics/AVX.hs
+++ b/x86/src/Data/Macaw/X86/Semantics/AVX.hs
@@ -7,14 +7,13 @@ import Control.Monad(forM_)
 import Data.Parameterized.NatRepr
 import Data.Parameterized.Some
 
-import Flexdis86.Register (ymmReg)
 import qualified Flexdis86 as F
 
 import Data.Macaw.CFG.Core(Value,bvValue)
-import Data.Macaw.Types(BVType,typeWidth,n0,n1,n32,n64,n256)
+import Data.Macaw.Types(BVType,typeWidth,n0,n1,n32,n64,n128, n256)
 
 import Data.Macaw.X86.InstructionDef
-import Data.Macaw.X86.Monad((.=), ymm, reg_high128, uext)
+import Data.Macaw.X86.Monad((.=), uext, subRegister)
 import Data.Macaw.X86.Getters(SomeBV(..),getSomeBVValue,getSomeBVLocation
                              , truncateBVValue )
 import Data.Macaw.X86.Generator(X86Generator, Expr(..),inAVX,evalArchFn,eval)
@@ -181,12 +180,12 @@ all_instructions =
     defNullary "vzeroall" $
       inAVX $
       forM_ [ 0 .. maxReg ] $ \r ->
-        ymm (ymmReg r) .= ValueExpr (bvValue 0)
+        subRegister n0   n256 (ZMM r) .= ValueExpr (bvValue 0)
 
   , defNullary "vzeroupper" $
       inAVX $
       forM_ [ 0 .. maxReg ] $ \r ->
-        reg_high128 (YMM r) .= ValueExpr (bvValue 0)
+        subRegister n128 n128 (ZMM r) .= ValueExpr (bvValue 0)
 
   , avxMov "vmovaps"
   , avxMov "vmovups"
diff --git a/x86/src/Data/Macaw/X86/X86Reg.hs b/x86/src/Data/Macaw/X86/X86Reg.hs
index ab0ed36f..9b0275db 100644
--- a/x86/src/Data/Macaw/X86/X86Reg.hs
+++ b/x86/src/Data/Macaw/X86/X86Reg.hs
@@ -31,6 +31,7 @@ module Data.Macaw.X86.X86Reg
   , X87_Control
   , XMM
   , YMM
+  , ZMM
 
     -- * X86Reg
   , X86Reg(..)
@@ -81,12 +82,12 @@ module Data.Macaw.X86.X86Reg
   , pattern X87_C2
   , pattern X87_C3
     -- * Large registers
-  , pattern YMM
+  , pattern ZMM
 
     -- * Register lists
   , gpRegList
   , flagRegList
-  , ymmRegList
+  , zmmRegList
   , x87FPURegList
   , x86StateRegs
   , x86CalleeSavedRegs
@@ -125,6 +126,7 @@ type X87_ControlMask = BVType 1
 type X87_Control     = BVType 2
 type XMM             = BVType 128
 type YMM             = BVType 256
+type ZMM             = BVType 512
 
 ------------------------------------------------------------------------
 -- X86Reg
@@ -144,8 +146,9 @@ data X86Reg tp
    | (tp ~ BVType 2)   => X87_TagReg {-# UNPACK #-} !Int
       -- One of 8 fpu/mmx registers.
    | (tp ~ BVType 80)  => X87_FPUReg {-#UNPACK #-} !F.MMXReg
-     -- One of 8 XMM/YMM registers
-   | (tp ~ BVType 256) => X86_YMMReg !F.YMMReg
+     -- AVX2 has 32 512-bit registers.
+   | (tp ~ BVType 512) => X86_ZMMReg !Word8
+
 
 instance Show (X86Reg tp) where
   show X86_IP          = "rip"
@@ -156,7 +159,7 @@ instance Show (X86Reg tp) where
   show X87_TopReg      = "x87top"
   show (X87_TagReg n)  = "tag" ++ show n
   show (X87_FPUReg r)  = show r
-  show (X86_YMMReg r)  = show r
+  show (X86_ZMMReg r)  = "zmm" ++ show r
 
 instance ShowF X86Reg where
   showF = show
@@ -205,11 +208,11 @@ instance OrdF X86Reg where
   compareF X87_TagReg{}       _                  = LTF
   compareF _                 X87_TagReg{}        = GTF
 
-  compareF (X87_FPUReg n)     (X87_FPUReg n')     = fromOrdering (compare n n')
+  compareF (X87_FPUReg n)     (X87_FPUReg n')    = fromOrdering (compare n n')
   compareF X87_FPUReg{}       _                  = LTF
   compareF _                 X87_FPUReg{}        = GTF
 
-  compareF (X86_YMMReg n)        (X86_YMMReg n')        = fromOrdering (compare n n')
+  compareF (X86_ZMMReg n)        (X86_ZMMReg n') = fromOrdering (compare n n')
 
 instance Ord (X86Reg cl) where
   a `compare` b = case a `compareF` b of
@@ -227,7 +230,7 @@ instance HasRepr X86Reg TypeRepr where
       X87_TopReg       -> knownRepr
       X87_TagReg{}     -> knownRepr
       X87_FPUReg{}     -> knownRepr
-      X86_YMMReg{}     -> knownRepr
+      X86_ZMMReg{}     -> knownRepr
 
 ------------------------------------------------------------------------
 -- Exported constructors and their conversion to words
@@ -359,8 +362,11 @@ pattern X87_C2 = X87_StatusReg 10
 pattern X87_C3 :: () => (t ~ X87_Status) => X86Reg t
 pattern X87_C3 = X87_StatusReg 14
 
-pattern YMM :: () => (t ~ YMM) => Word8 -> X86Reg t
-pattern YMM w = X86_YMMReg (F.YMMR w)
+pattern ZMM :: () => (t ~ ZMM) => Word8 -> X86Reg t
+pattern ZMM w <- X86_ZMMReg w
+  where ZMM w | w < 32 = X86_ZMMReg w
+              | otherwise = error "There are only 32 ZMM registers."
+
 
 x87StatusNames :: V.Vector String
 x87StatusNames = V.fromList $
@@ -392,8 +398,8 @@ x87TagRegList = [X87_TagReg i | i <- [0..7]]
 x87FPURegList :: [X86Reg (BVType 80)]
 x87FPURegList = [X87_FPUReg (F.mmxReg i) | i <- [0..7]]
 
-ymmRegList :: [X86Reg (BVType 256)]
-ymmRegList = [X86_YMMReg (F.ymmReg i) | i <- [0..15]]
+zmmRegList :: [X86Reg (BVType 512)]
+zmmRegList = [X86_ZMMReg i | i <- [0..31]]
 
 -- | List of registers stored in X86State
 x86StateRegs :: [Some X86Reg]
@@ -405,7 +411,7 @@ x86StateRegs
   ++ [Some X87_TopReg]
   ++ (Some <$> x87TagRegList)
   ++ (Some <$> x87FPURegList)
-  ++ (Some <$> ymmRegList)
+  ++ (Some <$> zmmRegList)
 
 type instance RegAddrWidth X86Reg = 64
 
@@ -444,11 +450,11 @@ x86CalleeSavedRegs = Set.fromList $
 x86ArgumentRegs :: [X86Reg (BVType 64)]
 x86ArgumentRegs = X86_GP <$> [ F.RDI, F.RSI, F.RDX, F.RCX, F.R8, F.R9 ]
 
-x86FloatArgumentRegs :: [X86Reg (BVType 256)]
-x86FloatArgumentRegs =  X86_YMMReg . F.ymmReg <$> [0..7]
+x86FloatArgumentRegs :: [X86Reg (BVType 512)]
+x86FloatArgumentRegs =  X86_ZMMReg <$> [0..7]
 
 x86ResultRegs :: [X86Reg (BVType 64)]
 x86ResultRegs = X86_GP <$> [ F.RAX, F.RDX ]
 
-x86FloatResultRegs :: [X86Reg (BVType 256)]
-x86FloatResultRegs = [ X86_YMMReg (F.ymmReg 0) ]
+x86FloatResultRegs :: [X86Reg (BVType 512)]
+x86FloatResultRegs = [ X86_ZMMReg 0 ]
diff --git a/x86_symbolic/src/Data/Macaw/X86/Crucible.hs b/x86_symbolic/src/Data/Macaw/X86/Crucible.hs
index 26e61da9..c9f51f17 100644
--- a/x86_symbolic/src/Data/Macaw/X86/Crucible.hs
+++ b/x86_symbolic/src/Data/Macaw/X86/Crucible.hs
@@ -105,7 +105,7 @@ withConcreteCountAndDir
   -> (AtomWrapper (RegEntry sym) M.BoolType)
   -> (S sym rtp bs r ctx -> (SymBV sym 64) -> IO (S sym rtp bs r ctx))
   -> IO (RegValue sym UnitType, S sym rtp bs r ctx)
-withConcreteCountAndDir state val_size wrapped_count wrapped_dir func = do
+withConcreteCountAndDir state val_size wrapped_count _wrapped_dir func = do
   let sym = state^.stateSymInterface
   let val_byte_size = M.repValSizeByteCount val_size
   bv_count <- toValBV sym wrapped_count
diff --git a/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs b/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
index f2d081e2..7c30211e 100644
--- a/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
+++ b/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
@@ -87,7 +87,7 @@ type instance ArchRegContext M.X86_64
    <+> (EmptyCtx ::> M.BVType 3)    -- X87 top of the stack (x87 status word)
    <+> CtxRepeat 8 (M.BVType 2)     -- X87 tags
    <+> CtxRepeat 8 (M.BVType 80)    -- FP regs
-   <+> CtxRepeat 16 (M.BVType 256)  -- YMM regs
+   <+> CtxRepeat 16 (M.BVType 512)  -- ZMM regs
 
 type RegAssign f = Assignment f (ArchRegContext M.X86_64)
 
@@ -112,7 +112,7 @@ x86RegName' (M.X87_StatusReg r) = show r
 x86RegName' M.X87_TopReg = "x87Top"
 x86RegName' (M.X87_TagReg r) = "x87Tag" ++ show r
 x86RegName' (M.X87_FPUReg r) = show r
-x86RegName' (M.X86_YMMReg r) = show r
+x86RegName' (M.X86_ZMMReg r) = "zmm" ++ show r
 
 x86RegName :: M.X86Reg tp -> C.SolverSymbol
 x86RegName r = C.systemSymbol $ "r!" ++ x86RegName' r
@@ -142,7 +142,8 @@ x86RegAssignment =
   <++> (Empty :> M.X87_TopReg)
   <++> (repeatAssign (M.X87_TagReg . fromIntegral)    :: Assignment M.X86Reg (CtxRepeat  8 (M.BVType 2)))
   <++> (repeatAssign (M.X87_FPUReg . F.mmxReg . fromIntegral) :: Assignment M.X86Reg (CtxRepeat  8 (M.BVType 80)))
-  <++> (repeatAssign (M.X86_YMMReg . F.ymmReg . fromIntegral) :: Assignment M.X86Reg (CtxRepeat 16 (M.BVType 256)))
+  <++> (repeatAssign (M.X86_ZMMReg . fromIntegral)
+        :: Assignment M.X86Reg (CtxRepeat 16 (M.BVType 512)))
 
 
 x86RegStructType :: C.TypeRepr (ArchRegStruct M.X86_64)