Verification of programs operating on mutable, heap-allocated data structures poses significant challenges due to potentially unbounded structures like linked lists and trees. In this paper, we present a novel relational heap encoding leveraging uninterpreted predicates and prophecy variables, reducing the task of verifying a program operating on heap data structures to the verification of a program operating on integers only. Our encoding of heap is general and not specific to any particular data structure. To the best of our knowledge, our approach is the first invariant-based method that achieves both soundness and completeness for heap-manipulating programs. We provide formal proofs establishing the correctness of our encodings. Through an experimental evaluation we demonstrate that our method significantly extends the capability of existing verification tools, allowing automatic verification of programs with heap that were previously out of reach for state-of-the-art tools.