[YICES-HELP] Ordering of constraints in Yices

[Avik Chaudhuri]

Whenever Yices takes a long time on a particular problem, I often find  
that reordering the constraints in the problem results in a dramatic  
speed-up (e.g., from several minutes to less than a second)!
Is there a known heuristic on ordering such constraints to get the  
best performance?
I find that arranging equalities before inequalities, and arranging  
"simple" equalities before "complex" equalities (e.g., those that  
involve arrays) works well, but that may be by chance or due to other  
specific factors.
It would be nice to know if there is something concrete backing up  
this intuition.

Thanks,
-Avik.