1; COMMAND-LINE: --rewrite-divk
2; EXPECT: sat
3(set-logic QF_NIA)
4(declare-fun x () Int)
5(declare-fun y () Int)
6(declare-fun z () Int)
7(assert (= (+ (* z 2) 1) (* x y)))
8(check-sat)
9(exit)
10