Is z3 model the same for a same program?

I would like to know if, for two exact same problems (same variables names, same assertions, same statements order, etc.), z3 will always return the same model, or if will change from time to time. If the z3 model can change under these constraints, is there any workaround yet so I can always get the same result ?

I've already read this but was looking for more actual answers : Z3 randomness of generated model values Z3 timing variation

Thanks in advance !