How to encode a scikit-learn Gradient Boosting Classifier as an SMT formula, using conditions on the sub-regressor for each class?

Question

I am trying to implement VeriGB, a tool for quantifying the ro- bustness of gradient boosted models during The Thirty-Third AAAI Conference on Artificial Intelligence (AAAI-19) by Gil Einziger, Maayan Goldstein, Yaniv Sa’ar, Itai Segall.

My problem is the following encoding of a classifier C:

In this encoding, they use the sub Regressor R_j for each class j of the problem. I am using scikit-learn on MNIST, so I have 10 classes and should be applying my function gamma (which I have implemented and is working well) on the corresponding regressors. How do I get these regressors?

My first though was using the estimators_ attribute, but it is of shape (n_estimators, n_classes), not the other way around. Could I build a regressor per class by iterating on each estimator?

Most other posts are trying to extract the rules of the classifiers or the sub trees, but I want the regressors, not their rules, in order to turn them into a formula for SMT.