  We present a tool for verification of deterministic programs with shared
mutable references against specifications such as assertions, preconditions,
postconditions, and read/write effects. We implement our tool by encoding
programs with mutable references into annotated purely functional recursive
programs. We then rely on function unfolding and the SMT solver Z3 to prove or
disprove safety and to establish program termination. Our tool uses a new
translation of programs where frame conditions are encoded using
quantifier-free formulas in first-order logic (instead of relying on
quantifiers or separation logic). This quantifier-free encoding enables SMT
solvers to prove safety or report counterexamples relative to the semantics of
procedure specifications. Our encoding is possible thanks to the expressive
power of the extended array theory of the Z3 SMT solver. In addition to the
ability to report counterexamples, our tool retains efficiency of reasoning
about purely functional layers of data structures, providing expressiveness for
mutable data but also a significant level of automation for purely functional
aspects of software. We illustrate our tool through examples manipulating
mutable linked structures and arrays.
