summaryrefslogtreecommitdiff
path: root/test/regress/regress0/quantifiers/macros-int-real.smt2
blob: d29ddfe8f292bbc0a6b75e77dc6419783bcb31be (plain) 
1
2
3
4
5
6
7
8
9

; COMMAND-LINE: --macros-quant
; EXPECT: unknown
(set-logic AUFLIRA)

(declare-fun round2 (Real) Int)
(assert (forall ((i Int))  (= (round2 (to_real i)) i)))

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