summaryrefslogtreecommitdiff
path: root/test/regress/regress0/fp/issue6164.smt2
blob: 056a98afc6822331a2f1709f4769da92e04e8204 (plain) 
1
2
3
4
5
6
7

; REQUIRES: symfpu
; EXPECT: sat
; EXPECT: ((((_ to_fp 5 11) roundNearestTiesToAway (/ 1 10)) (fp #b0 #b01011 #b1001100110)))
(set-logic ALL)
(set-option :produce-models true)
(check-sat)
(get-value (((_ to_fp 5 11) RNA 0.1)))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback