fixes

ir/memory.cpp

@@ -1275,6 +1275,11 @@ void Memory::mkAxioms(const Memory &tgt) const {
     state->addAxiom(Pointer::mkNullPointer(tgt).blockAlignment() == -1u);
   }
 
+  for (unsigned bid = has_null_block; bid < num_nonlocals; ++bid) {
+    Pointer p(bid < num_nonlocals_src ? *this : tgt, bid, false);
+    state->addAxiom(p.blockSize() != 0);
+  }
+
   for (unsigned bid = 0; bid < num_nonlocals_src; ++bid) {
     if (skip_bid(bid))
       continue;
@@ -1312,8 +1317,7 @@ void Memory::mkAxioms(const Memory &tgt) const {
     auto sz    = p1.blockSize().zextOrTrunc(bits_ptr_address);
     auto align = p1.blockAlignment();
 
-    if (!has_null_block || bid != 0)
-      state->addAxiom(addr != zero);
+    state->addAxiom(addr != zero);
 
     // address must be properly aligned
     auto align_bytes = one << align.zextOrTrunc(bits_ptr_address);
@@ -1786,8 +1790,6 @@ Memory::alloc(const expr *size, uint64_t align, BlockKind blockKind,
     // support for 0-sized arrays like [0 x i8], which are arbitrarily sized
     if (size)
       state->addAxiom(p.blockSize() == size_zext);
-    else
-      state->addAxiom(p.blockSize().uge(1));
     state->addAxiom(p.isBlockAligned(align, true));
     state->addAxiom(p.getAllocType() == alloc_ty);
 
@@ -2401,7 +2403,7 @@ Memory Memory::mkIf(const expr &cond, Memory &&then, Memory &&els) {
 void Memory::print_array(ostream &os, const expr &a, unsigned indent) const {
   expr idx, val, a2, cond, then, els;
   if (a.isConstArray(val)) {
-    os << "else: " << Byte(*this, std::move(val)) << '\n';
+    os << "*: " << Byte(*this, std::move(val)) << '\n';
   }
   else if (a.isStore(a2, idx, val)) {
     idx.printUnsigned(os);