blob: 5e3c2952b7b58ffc0b66c2bb2027973671dc96c5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
; COMMAND-LINE: --fmf-bound
; EXPECT: sat
(set-logic ALL)
(declare-datatypes ((list 0)) (((cons (head Int) (tail list)) (nil))))
(declare-fun P (Int) Bool)
(declare-fun S () (Set list))
; can use simple unification to infer bounds on x and y
(assert (forall ((x Int) (y list)) (=> (member (cons x y) S) (P x))))
(assert (member (cons 4 (cons 1 nil)) S))
(assert (member (cons 2 nil) S))
; should construct instantiation involving selectors for l
(declare-fun l () list)
(assert ((_ is cons) l))
(assert (member l S))
; should not contribute to instantiations
(assert (member nil S))
(assert (not (P 1)))
(assert (not (P 0)))
(check-sat)
|
