From 8942e1a346ce9be67b36a75fa38f668377c194ec Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Mon, 3 Feb 2025 12:11:32 -0500
Subject: [PATCH] Slightly strengthen/simplify normalization test

---
 what4/test/Bool.hs | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/what4/test/Bool.hs b/what4/test/Bool.hs
index fd43fce7..2c138b09 100644
--- a/what4/test/Bool.hs
+++ b/what4/test/Bool.hs
@@ -199,7 +199,7 @@ isNormalConjunct ::
   Either String ()
 isNormalConjunct sym expr pol =
   case expr of
-    BoolExpr {} -> Right ()
+    BoolExpr {} -> Left "boolean literal inside conjunction"
     BoundVarExpr {} -> Right ()
     AppExpr ae ->
       case appExprApp ae of
@@ -230,11 +230,9 @@ isNormal sym =
     BoundVarExpr {} -> Right ()
     AppExpr ae ->
       case appExprApp ae of
-        NotPred (asApp -> Just (ConjPred cm)) -> isNormalMap sym cm
-        ConjPred cm -> isNormalMap sym cm
-
         NotPred (asApp -> Just NotPred {}) -> Left "double negation"
         NotPred e -> isNormal sym e
+        ConjPred cm -> isNormalMap sym cm
         BaseIte BaseBoolRepr _sz c l r -> isNormalIte sym c l r
         _ -> Left "non-normal app"
     _ -> Left "non-normal expr"