summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sygus/issue3634.smt2
blob: ad691077356bf2509aa2c33ddc74e5b111aea27e (plain) 
1
2
3
4
5
6
7

; EXPECT: sat
; COMMAND-LINE: --sygus-inference -q
(set-logic ALL)
(declare-fun a () Int)
(declare-fun b () Real)
(assert (= (/ 1 (to_real a)) b))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback