Can anyone comment on the relative feasibility of using Z3 for problems of similar or greater scale? The performance is actually kind of concerning.
The heuristics can be hierarchical permitting customized implementations, see 'IndomainHierarchical' here: http://jacopguide.osolpro.com/guideJaCoP.html#x1-820001
What's interesting about JaCoP in particular is because it has derivative, and Multivariate Interval Newton Method constraints. If you can model your problem in terms of 'flow', you'll eliminate the risk of calculating beyond INT_MAX, in case that's a concern. Reference: http://jacopguide.osolpro.com/guideJaCoP.html#x1-490005
And that's just JaCoP, there are many great constraint solvers out there.