sig
  val mk_polynomial_subresultants :
    Z3.context ->
    Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr list
end