Symbolic execution is a technique frequently used to reason about code. In symbolic execution, an analyzer keeps track of the program state’s logic representation and validates the correctness of state transitions. This verification is usually discharged to SMT solvers as queries to the logical state.

Separation logic is frequently used to express and verify properties of programs with pointers or references. However, most SMT solvers (like Z3) do not support separation logic natively. Recently, the CVC5 SMT solver has introduced support for a decidable fragment of separation logic, which has not yet been integrated into more high-level tools.

This work aims to address this gap, by providing a proof of concept for implementing the Frame Rule using SMT queries to mentioned solver. We conclude that this encoding can simplify the machinery dealing with separation logic, such as that present in tools verifying separation logic with symbolic execution like Smallfoot or GRASShopper.