test/regress/regress0/arith/ite-lift.smt2


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

; COMMAND-LINE: --check-proofs
(set-option :incremental false)
(set-info :status unsat)
(set-info :category "crafted")
(set-info :difficulty "0")
(set-logic QF_LRA)

(declare-fun x_0 () Real)
(declare-fun x_1 () Real)
(declare-fun b_f () Bool)
(assert (<= x_0 0))
(assert (<= x_1 0))
(assert (not b_f))
(assert (ite b_f b_f (>= (+ x_0 x_1) 1)))
(check-sat)