Как реализовать собственную тактику упрощения в Z3?

В своем инструменте я использую условия, которые сравнивают константы с целочисленными переменными (например, y < 100). Часто существует несколько условий для одной переменной, и я хочу упростить эти случаи. Например: у < 100 && у! = 99 должно стать у < 99. Тактика упрощения не делает этого, и ни один из аргументов в пользу упрощения не может помочь.

В коде:

context c;
goal g(c);
expr x = c.int_const("x");
expr y = c.int_const("y");
solver s(c);
expr F = y < 100 && y != 99;
g.add(F);
tactic t = tactic(c, "simplify");
apply_result r = t(g);
for (unsigned i = 0; i < r.size(); i++) {
std::cout << "subgoal " << i << "\n" << r[i] << "\n";
}

Выход в конце возвращает: subgoal 0
(goal
(not (<= 100 y))
(not (= y 99)))

и не subgoal 0(goal(not(<= 99 y)) или что-то похожее, как я хочу.

Поэтому я хочу реализовать свою собственную упрощенную тактику. К сожалению, я не могу найти, как это сделать. Я знаю, что эта тактика должна быть реализована в C ++, но как я могу представить свою тактику в Z3?