I’m trying to solve an SMT problem containing linear integer modulo theory with Z3 (Python). The problem is similar to the “Learning a Boolean Function” example on pp. 14f of Knuth’s satisfiability book. My problem has a set of Boolean-valued formulas (hundreds), each containing the same set of unknown integer and Boolean variables to be solved for (tens), and the optimization objective is to maximize the number of true formulas as a function of these unknowns. I’m trying to improve the solution speed. The formulas contain mixed Boolean variables with expressions like (x <= const) or (x1 + x2 <= const) or (x == x1 + x2) for integers x, x1, x2, const.