blob: 146487925b082aca6acde3f9aea50972d05d6806 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
; COMMAND-LINE: --fmf-bound-int
; EXPECT: sat
(set-logic UFLIA)
(set-info :status sat)
(declare-sort U 0)
(declare-sort V 0)
(declare-fun P (U Int V Int U Int) Bool)
(assert (forall ((x U) (y Int) (z V) (w Int) (v U) (d Int)) (=> (and (<= 0 d 1) (<= 2 y 6) (<= 40 w (+ 37 y))) (P x y z w v d))))
(declare-fun a () U)
(declare-fun b () V)
(assert (not (P a 2 b 40 a 0)))
(assert (not (P a 6 b 39 a 0)))
(assert (not (P a 6 b 44 a 0)))
(check-sat)
|
