improve translation of div and mod for SMT solvers
A feedback from AdaCore : changing the translation of div
and mod
(both euclidean and computer) into what is currently commented out in the driver improves, in particular for counterexamples. It applies to Z3 as well.