fix #961: input ptrs cannot be stack allocated

Add a precondition for that. This test is hard to reproduce because it
relies on an optimization not being done just in target, while done in source.

ir/memory.cpp

@@ -1313,6 +1313,7 @@ expr Memory::mkInput(const char *name, const ParamAttrs &attrs0) {
   auto bid = p.getShortBid();
 
   state->addAxiom(bid.ule(max_bid));
+  state->addAxiom(!Pointer(*this, max_bid, false).isStackAllocated(false));
 
   AliasSet alias(*this);
   alias.setMayAliasUpTo(false, max_bid);

ir/pointer.cpp

@@ -502,11 +502,11 @@ expr Pointer::getAllocType() const {
                    expr::mkUInt(0, 2));
 }
 
-expr Pointer::isStackAllocated() const {
+expr Pointer::isStackAllocated(bool simplify) const {
   // 1) if a stack object is returned by a callee it's UB
   // 2) if a stack object is given as argument by the caller, we can upgrade it
   //    to a global object, so we can do POR here.
-  if (!has_alloca || isLocal().isFalse())
+  if (simplify && (!has_alloca || isLocal().isFalse()))
     return false;
   return getAllocType() == STACK;
 }

ir/pointer.h

@@ -116,7 +116,7 @@ class Pointer {
     CXX_NEW,
   };
   smt::expr getAllocType() const;
-  smt::expr isStackAllocated() const;
+  smt::expr isStackAllocated(bool simplify = true) const;
   smt::expr isHeapAllocated() const;
   smt::expr isNocapture(bool simplify = true) const;
   smt::expr isNoRead() const;