simplify mkAxioms: remove implied constraints

found bby Juneyoung Lee

Author: nunoplopes

ir/memory.cpp

@@ -1540,26 +1540,6 @@ void Memory::mkAxioms(const Memory &tgt) const {
     }
     state->addAxiom(p1.isBlockAlive().implies(disj));
   }
-
-  // ensure locals fit in their reserved space
-  expr one = expr::mkUInt(1, bits_size_t - 1);
-  auto locals_fit = [&one](const Memory &m) {
-    auto sum = expr::mkUInt(0, bits_size_t - 1);
-    for (unsigned bid = 0, nlocals = m.numLocals(); bid < nlocals; ++bid) {
-      Pointer p(m, bid, true);
-      if (auto sz = m.local_blk_size.lookup(p.getShortBid())) {
-        auto size = sz->extract(bits_size_t - 2, 0);
-        auto align = one << p.blockAlignment().zextOrTrunc(bits_size_t - 1);
-        align = align - one;
-        auto sz_align = size + align;
-        m.state->addPre(size.add_no_uoverflow(align));
-        m.state->addPre(sum.add_no_uoverflow(sz_align));
-        sum = sum + sz_align;
-      }
-    }
-  };
-  locals_fit(*this);
-  locals_fit(tgt);
 }
 
 void Memory::resetGlobals() {
@@ -1784,7 +1764,6 @@ static expr disjoint_local_blocks(const Memory &m, const expr &addr,
   auto one = expr::mkUInt(1, 1);
   auto zero = expr::mkUInt(0, bits_for_offset);
   for (auto &[sbid, addr0] : blk_addr) {
-    (void)addr0;
     Pointer p2(m, prepend_if(one, expr(sbid), ptr_has_local_bit()), zero);
     disj &= p2.isBlockAlive()
               .implies(disjoint(addr, sz, p2.getAddress(), p2.blockSize()));