only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
hide internal constants z3div and z3mod;
rewrite div/mod to z3div/z3mod instead of adding extra rules characterizing div/mod in terms of z3div/z3mod
use "../settings";
use_thy "termination";
use_thy "Induction";
use_thy "Nested1";
use_thy "Nested2";