Bump What4 submodule, adapt to BoolMap changes (#1306)

GaloisInc · Feb 12, 2025 · 50d1550 · 50d1550
1 parent f84675d
commit 50d1550
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git 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
+1 −0		.github/workflows/gen_matrix.pl
+13 −6		.github/workflows/test.yml
+1 −1		dependencies/aig
+1 −1		what4-abc/what4-abc.cabal
+1 −1		what4-blt/what4-blt.cabal
+1 −1		what4-transition-system/what4-transition-system.cabal
+11 −0		what4/CHANGES.md
+26 −23		what4/src/What4/Expr/App.hs
+110 −16		what4/src/What4/Expr/BoolMap.hs
+34 −18		what4/src/What4/Expr/Builder.hs
+1 −10		what4/src/What4/Expr/GroundEval.hs
+5 −5		what4/src/What4/Expr/VarIdentification.hs
+2 −2		what4/src/What4/Expr/WeightedSum.hs
+5 −5		what4/src/What4/Protocol/SMTWriter.hs
+1 −1		what4/src/What4/Protocol/VerilogWriter/Backend.hs
+1 −1		what4/src/What4/Serialize/Printer.hs
+0 −1		what4/src/What4/Solver/CVC5.hs
+3 −4		what4/src/What4/Utils/AnnotatedMap.hs
+2 −2		what4/src/What4/Utils/Environment.hs
+4 −2		what4/src/What4/Utils/Word16String.hs
+295 −0		what4/test/Bool.hs
+62 −0		what4/test/BoolNormalization.hs
+3 −0		what4/test/ExprsTest.hs
+0 −1		what4/test/InvariantSynthesis.hs
+4 −1		what4/test/OnlineSolverTest.hs
+13 −2		what4/what4.cabal