Z3's implementation of isTrue is

  protected boolean isTrue(Long pParam) {
    return isOP(z3context, pParam, Z3_decl_kind.Z3_OP_TRUE);
  }

which in turn does at least 3 native calls.
Wouldn't it suffice to do the following?

  protected boolean isTrue(Long pParam) {
    return pParam.equals(z3True); // Z3 should only have a single instance of "true".
  }

Maybe there is a possibility to have multiple copies of the true value?

The reason that I'm asking is that the first implementation is considerably slower and it is very noticable when tracking the solver with the user propagators from #349. Indeed, on an Nqueens + propagator example, 1/3 (70 seconds!) of all time is spent just executing the isTrue function. The proposed solution is faster by at least two orders of magnitude.
I can fix this bottleneck directly in the user propagator (by just not using isTrue) but I would rather have a solution that benefits everyone (considering that isTrue/isFalse is called internally in many places).