summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sep/finite-witness-sat.smt2
blob: 93413d950fdd8cd1c4da32c8f305fe21d97019c6 (plain) 
1
2
3
4
5
6
7
8
9
10
11

; COMMAND-LINE: --finite-model-find --quant-epr --no-check-models
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(declare-sort Loc 0)
(declare-const l Loc)

(assert (not (emp l)))
(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