More

ajreynol · Feb 22, 2025 · 844a45d · 844a45d
1 parent 80701f2
commit 844a45d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/theory/bv/macro_rewrite_elaborator.cpp b/src/theory/bv/macro_rewrite_elaborator.cpp
@@ -40,14 +40,14 @@ bool MacroRewriteElaborator::ensureProofFor(CDProof* cdp,
   {
     case ProofRewriteRule::MACRO_BV_OR_SIMPLIFY:
     case ProofRewriteRule::MACRO_BV_AND_SIMPLIFY:
+    case ProofRewriteRule::MACRO_BV_XOR_SIMPLIFY:
       return ensureProofForSimplify(cdp, eq);
     case ProofRewriteRule::MACRO_BV_CONCAT_EXTRACT_MERGE:
     case ProofRewriteRule::MACRO_BV_CONCAT_CONSTANT_MERGE:
       return ensureProofForConcatMerge(cdp, eq);
     case ProofRewriteRule::MACRO_BV_EXTRACT_CONCAT:
     case ProofRewriteRule::MACRO_BV_EXTRACT_SIGN_EXTEND:
     case ProofRewriteRule::MACRO_BV_ASHR_BY_CONST:
-    case ProofRewriteRule::MACRO_BV_XOR_SIMPLIFY:
     case ProofRewriteRule::MACRO_BV_AND_OR_XOR_CONCAT_PULLUP:
     case ProofRewriteRule::MACRO_BV_MULT_SLT_MULT:
     case ProofRewriteRule::MACRO_BV_FLATTEN_ASSOC_COMMUT: break;