summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sygus/issue3944-div-rewrite.smt2
blob: 78035790b0830ea1aeb2d15732831b405399aed6 (plain) 
1
2
3
4
5
6
7
8
9
10
11

; EXPECT: sat
; COMMAND-LINE: --sygus-inference
(set-logic ALL)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(assert (= c d))
(assert (> (+ a (div 0 b)) c))
(assert (= b (- 1)))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback