1 2 3 4 5 6 7 8 9 10 11
; EXPECT: sat ; COMMAND-LINE: --sygus-inference -q (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)