fix rewriting polynomials

        Return a mapping from new symbols to replaced expressions.

        Note: performs formula rewritings before the replacement.

        """

        if not exprs_from:

            return expr_to

        exprs_from = exprs_from or []

        try:

            re = Tactic("elim-term-ite")(_rewrite_sext(_desimplify_ext(expr_to)))

            assert len(re) == 1, re

                        P1.add(P2)

                        simple_poly.append(P1)

            if not simple_poly:

                return expr_to

            # print('--------')

            # for p in simple_poly:

            #    print('  > ASSUM', _desimplify_ext(simplify(p.expr())))

        return Expr(expr, ty)

    def rewrite_polynomials(self, from_exprs):

        expr = rewrite_polynomials(self.unwrap(), map(lambda x: x.unwrap(), from_exprs))

        expr = rewrite_polynomials(self.unwrap(), map(lambda x: x.unwrap(), from_exprs) if from_exprs else None)

        if expr is None:

            return self

        return Expr(expr, self.type())

        yield (k, v)

def _rewrite_poly(em, exprs, assumptions=None):

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

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

    if assumptions:

        A = []

        for i in range(len(assumptions)):