revert 9863f75

It turns out these simplifications of SMT exprs don't help

Author: nunoplopes

ir/memory.cpp

@@ -474,7 +474,6 @@ static StateValue bytesToValue(const Memory &m, const vector<Byte> &bytes,
     // A zero integer byte is considered as a null pointer byte with any byte
     // offset.
     expr non_poison = true;
-    AndExpr ptr_constrs, non_ptr_constrs;
 
     for (unsigned i = 0, e = bytes.size(); i < e; ++i) {
       auto &b = bytes[i];
@@ -487,13 +486,12 @@ static StateValue bytesToValue(const Memory &m, const vector<Byte> &bytes,
       } else {
         non_poison &= is_ptr == b_is_ptr;
       }
-      ptr_constrs.add(b.ptrByteoffset() == i);
-      ptr_constrs.add(ptr_value == loaded_ptr);
-      non_ptr_constrs.add(b.nonptrValue() == 0);
-
+      non_poison &=
+        expr::mkIf(is_ptr,
+                   b.ptrByteoffset() == i && ptr_value == loaded_ptr,
+                   b.nonptrValue() == 0);
       non_poison &= !b.isPoison();
     }
-    non_poison &= expr::mkIf(is_ptr, ptr_constrs(), non_ptr_constrs());
 
     // if bits of loaded ptr are a subset of the non-ptr value,
     // we know they must be zero otherwise the value is poison.
@@ -1775,7 +1773,6 @@ StateValue Memory::load(const Pointer &ptr, const Type &type, set<expr> &undef,
   // partial order reduction for fresh pointers
   // can alias [0, next_ptr++] U extra_tgt_consts
   if (is_ptr && !val.non_poison.isFalse()) {
-    AndExpr constr;
     optional<unsigned> max_bid;
     for (auto &p : all_leaf_ptrs(*this, val.value)) {
       auto islocal = p.isLocal();
@@ -1789,15 +1786,10 @@ StateValue Memory::load(const Pointer &ptr, const Type &type, set<expr> &undef,
           for (unsigned i = num_nonlocals_src; i < numNonlocals(); ++i) {
             I->second.setMayAlias(false, i);
           }
-
-          expr c = islocal || bid.ule(*max_bid);
-          if (numNonlocals() > num_nonlocals_src)
-            c |= bid.uge(num_nonlocals_src) && bid.ule(numNonlocals()-1);
-          constr.add(std::move(c));
+          state->addPre(!val.non_poison || islocal || bid.ule(*max_bid));
         }
       }
     }
-    state->addPre(val.non_poison.implies(constr()));
   }
 
   return val;