summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sep/sep-fmf-priority.smt2
blob: d916a50e529876b4e21f4f82bbc95e97a4358fc8 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13

; COMMAND-LINE: --finite-model-find --quant-epr
; 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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback