Separation Logic
From CVC4
Logic
CVC4 supports a syntax for separation logic as an extension of the *.smt2 language. To enable separation logic, use the "all supported" logic:
(set-logic ALL_SUPPORTED)
Syntax
The syntax for the operators of separation logic (points-to, emp, star, wand) is as follows:
