1 2 3 4 5 6 7 8 9 10 11 12 13
; COMMAND-LINE: --finite-model-find --quant-epr --no-check-models ; EXPECT: sat (set-logic ALL_SUPPORTED) (declare-sort Loc 0) (declare-const l Loc) (declare-const x Loc) (declare-heap (Loc Loc)) (assert (wand (pto x x) false)) (assert (forall ((x Loc) (y Loc)) (not (pto x y)))) (check-sat)