Yices2 does support modulo with constants.
At least partial non-linear arithmetic is supported.
@@ -116,7 +116,7 @@ public class NonLinearArithmeticWithModuloTest extends SolverBasedTest0 {
imgr.makeNumber(1),
handleExpectedException(() -> imgr.modulo(a, imgr.makeNumber(3)))));
- if (ImmutableSet.of(Solvers.SMTINTERPOL, Solvers.CVC4).contains(solver)
+ if (ImmutableSet.of(Solvers.SMTINTERPOL, Solvers.CVC4, Solvers.YICES2).contains(solver)
&& nonLinearArithmetic == NonLinearArithmetic.APPROXIMATE_FALLBACK) {
// some solvers support modulo with constants
assertThatFormula(f).isUnsatisfiable();
