test/regress/regress0/quantifiers/mix-complete-strat.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

; COMMAND-LINE: --finite-model-find
; EXPECT: sat
(set-logic UFLIA)
(set-info :status sat)

(declare-sort U 0)
(declare-fun P (U) Bool)

(assert (forall ((x U)) (P x)))

(declare-fun u () U)
(assert (P u))

(declare-const a Int)
(declare-const b Int)
(assert (forall ((x Int)) (or (> x a) (< x b))))

(check-sat)