diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs
index 21c8259e8..f093e8d5f 100644
--- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs
+++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs
@@ -172,7 +172,7 @@ explainCex sym bbMap evalFn =
 
       -- We expect at least one of the contained predicates to be false, so choose one
       -- and explain that failure
-      (asApp -> Just (ConjPred (viewBoolMap -> BoolMapTerms tms))) -> go (Fold.toList tms)
+      (asApp -> Just (ConjPred (viewConjMap -> Conjuncts tms))) -> go (Fold.toList tms)
         where
         go [] = pure NoExplanation
         go ((x,Positive):xs)
@@ -223,7 +223,7 @@ explainCex sym bbMap evalFn =
 
       -- under negative polarity, we expect all members of the disjunction to be false,
       -- and we must construct an explanation for all of them
-      (asApp -> Just (ConjPred (viewBoolMap -> BoolMapTerms tms))) -> go (Fold.toList tms) NoExplanation
+      (asApp -> Just (ConjPred (viewConjMap -> Conjuncts tms))) -> go (Fold.toList tms) NoExplanation
         where
         go [] es = pure es
         go ((x,Positive):xs) es =
diff --git a/dependencies/what4 b/dependencies/what4
index 94613390a..ebf9ac050 160000
--- a/dependencies/what4
+++ b/dependencies/what4
@@ -1 +1 @@
-Subproject commit 94613390a1bbd8b08cdb4272d85884943b63286a
+Subproject commit ebf9ac050c4ef5a5fda880e2e92cf76e14028ad2