如何使用c++为z3中已有的声明函数添加新的约束？

#include <z3++.h>

z3::context ctx;

z3::func_decl existingFunc = ctx.function("existingFunc", ctx.int_sort(), ctx.bool_sort());

z3::expr newConstraint = existingFunc(ctx.int_const("x")) && existingFunc(ctx.int_const("y"));

z3::solver solver(ctx);
solver.add(newConstraint);

z3::check_result result = solver.check();
if (result == z3::sat) {
    // 约束可满足的处理逻辑
    z3::model model = solver.get_model();
    // 获取满足约束的变量赋值
    z3::expr xValue = model.eval(ctx.int_const("x"));
    z3::expr yValue = model.eval(ctx.int_const("y"));
} else if (result == z3::unsat) {
    // 约束不可满足的处理逻辑
} else {
    // 求解过程出错的处理逻辑
}