summaryrefslogtreecommitdiff
path: root/test/regress/regress0/quantifiers/bug749-rounding.smt2
blob: 5fea8d4fffc44478f90ec12c5c10de16ae5102fe (plain) 
1
2
3
4
5
6
7
8
9
10
11

; COMMAND-LINE: --var-ineq-elim-quant
; EXPECT: unknown
(set-logic UFLIRA)

(declare-fun round2 (Real) Int)

(assert (forall ((x Real) (i Int)) (=> (<= x (to_real i)) (<= (round2 x) i)) ))
(assert (forall ((x Real) (i Int)) (=> (<= (to_real i) x) (<= i (round2 x))) ))


(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback