The search method is propagate constraints for a while then pick a variable and bisect it, solve each side and combine.
Generalising slightly from your suggestion, varying the order in which the search runs, and whether various propagations or optimisations are active, should only change runtime and not the set of results.
The other thing I've discovered since that project is clang's AST based branch coverage recording. Getting to the point where smallish unit tests that can be perturbed as above or enumerated exercise each path through the solver would probably shake out the bugs.
The search method is propagate constraints for a while then pick a variable and bisect it, solve each side and combine.
Generalising slightly from your suggestion, varying the order in which the search runs, and whether various propagations or optimisations are active, should only change runtime and not the set of results.
The other thing I've discovered since that project is clang's AST based branch coverage recording. Getting to the point where smallish unit tests that can be perturbed as above or enumerated exercise each path through the solver would probably shake out the bugs.