diff --git a/deps/macaw b/deps/macaw
index 2bd0633ba8..cd5dfe8c65 160000
--- a/deps/macaw
+++ b/deps/macaw
@@ -1 +1 @@
-Subproject commit 2bd0633ba83a2bfb4fb6c7ca6f61d419bdae7565
+Subproject commit cd5dfe8c659d7d9eb2fbed8eaa922eaaa8cc3e1c
diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs
index 28f4ae7080..85cd09f8b4 100644
--- a/src/SAWScript/Crucible/LLVM/X86.hs
+++ b/src/SAWScript/Crucible/LLVM/X86.hs
@@ -201,18 +201,13 @@ cryptolUninterpreted ::
   SharedContext ->
   [Term] ->
   m Term
-cryptolUninterpreted env nm sc xs@[_, _] =
+cryptolUninterpreted env nm sc xs =
   case lookupIn nm $ eTermEnv env of
     Left _err -> throwX86 $ mconcat
       [ "Failed to lookup Cryptol name \"", nm
       , "\" in Cryptol environment"
       ]
     Right t -> liftIO $ scApplyAll sc t xs
-cryptolUninterpreted _ nm _ xs = throwX86 $ mconcat
-  [ "Type error in call to \"", nm
-  , "\": Expected 2 arguments, given ", show $ length xs
-  , " arguments"
-  ]
 
 -------------------------------------------------------------------------------
 -- ** Entrypoint
@@ -248,6 +243,7 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se
       liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesDec sfs) $ cryptolUninterpreted cenv "aesdec"
       liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesDecLast sfs) $ cryptolUninterpreted cenv "aesdeclast"
       liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesKeyGenAssist sfs) $ cryptolUninterpreted cenv "aeskeygenassist"
+      liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnAesIMC sfs) $ cryptolUninterpreted cenv "aesimc"
       liftIO $ C.sawRegisterSymFunInterp sym (Macaw.fnClMul sfs) $ cryptolUninterpreted cenv "clmul"
 
       let preserved = Set.fromList . catMaybes $ stringToReg . Text.toLower . Text.pack <$> rwPreservedRegs rw