solver: rewrite polynomials always

        if r is not None:

            return r

        # First try to rewrite the formula into simpler form

        # First try to rewrite the formula into a simpler form

        expr1 = em.conjunction(*exprs).rewrite_polynomials(assumptions)

    else:

        expr1 = em.conjunction(*exprs).rewrite_polynomials(exprs)

    if expr1 is None:

        expr = em.conjunction(*assumptions, *exprs)

    else:

        A = []

        for i in range(len(assumptions)):

            a = assumptions[i]

            A.append(

                a.rewrite_polynomials([x for n, x in enumerate(assumptions) if n != i])

            )

            ra = a.rewrite_polynomials(assumptions)

            if ra is None:

                # we failed

                A = assumptions

                break

            A.append(ra)

        assumptions = A

        r = IncrementalSolver().try_is_sat(to1, *assumptions, expr1)

        if r is not None:

            return r

        expr = em.conjunction(*assumptions, expr1)

    else:

        expr = em.conjunction(*assumptions, *exprs)

    ###

    # Now try abstractions