Minor

ajreynol · Feb 22, 2025 · 17c7a96 · 17c7a96
1 parent 9ad138e
commit 17c7a96
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/theory/bv/macro_rewrite_elaborator.cpp b/src/theory/bv/macro_rewrite_elaborator.cpp
@@ -279,6 +279,7 @@ bool MacroRewriteElaborator::ensureProofForMultSltMult(CDProof* cdp,
         size_t sz = utils::getSize(n[0]);
         if (n[0] == utils::mkZero(sz))
         {
+          // turn concatenation with zero into zero extend
           Node zext = nm->mkConst(BitVectorZeroExtend(sz));
           Node nze = nm->mkNode(zext, n[1]);
           tcpg.addRewriteStep(n, nze, nullptr, false, TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE);
@@ -290,6 +291,7 @@ bool MacroRewriteElaborator::ensureProofForMultSltMult(CDProof* cdp,
     }
     if (ch[1].getKind()==Kind::BITVECTOR_ZERO_EXTEND)
     {
+      Assert (ch[0].getKind()!=Kind::BITVECTOR_ZERO_EXTEND);
       // swap to match rule
       Node mul = nm->mkNode(eq[0][i].getKind(), ch[0], ch[1]);
       Node muls = nm->mkNode(eq[0][i].getKind(), ch[1], ch[0]);