summaryrefslogtreecommitdiff
path: root/test/regress/regress1/fmf/fmf-bound-int.smt2
blob: fb3106bdf4fb8478cdf5778c296631986faed061 (plain) 
1
2
3
4
5
6
7

; COMMAND-LINE: --finite-model-find --fmf-bound-int
; EXPECT: sat
(set-logic UFLIA)
(declare-fun P (Int Int) Bool)
(declare-fun Q (Int) Bool)
(assert (forall ((x Int)) (=> (and (<= 0 x) (<= x (ite (P 0 0) 10 20))) (Q x))))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback