path: root/test/regress/regress1/bug516.smt2

; COMMAND-LINE: --finite-model-find --fmf-bound-int -q
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)
(set-option :incremental true)
(declare-fun P (Int) Bool)
(declare-fun ten () Int)

(assert (forall ((x Int)) (=> (<= 1 x ten) (P x))))

(push)
(assert (= ten 10))

(check-sat)
(pop)