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 !
Almost; the default tactics in Z3 use timers and sometimes it happens that they produce something important just before a timer aborts something, or that it just doesn't get it. Apart from that, the performance should be fairly stable, and you can replace the default tactics with your own that don't use timers.
Of course, this does not hold for different versions of Z3, i.e., if you compile tomorrows version you may get very different behaviour in comparison to today's.
