(Per discussion with @nikolaj_bjorner on email) The answer is because / is Real division while div is Int division.

So

(assert (>= b 32))
(assert (= a (div b 8)))  
(assert (not (= (div b a) 8))) 

is SAT with a = 4 and b = 37 , and so
* div b 8 is 4 but
* div b a is 9

OTOH the version with / is unsat because
1. The solvers automatically coerce the Int arguments to Real to enable / but
2. The define-fun is rejected because (/ x y) cannot be coerced down to Int