title: Support for integer division in SMT solvers
body: <p>I have executed z3 and CVC4 on the following SMT input. Both return unknown.</p>
  <pre><code>;!(a,b,c).(0&lt;=a &amp; 0&lt;=b &amp; 1&lt;=c
  ;               =&gt;
  ;               (a+(b mod c)) mod c = (a+b) mod c)
  ;
  ;
  (set-logic NIA)
  (set-option :print-success false)
  
  (declare-fun a () Int)
  (declare-fun b () Int)
  (declare-fun c () Int)
  
  (assert (&lt;= 0 a))
  (assert (&lt;= 1 c))
  (assert (&lt;= 0 b))
  
  (assert (! (not (= (mod (+ a (mod b c)) c) (mod (+ a b) c))) :named goal))
  (check-sat)
  (exit)
  </code></pre>
  <ul>
  <li><p>Is there any fundamental reason why they are not able to decide satisfiability?</p>
  </li>
  <li><p>Which options or other solvers would be suitable to address this kind of problems?</p>
  </li>
  </ul>