Tighter integration of Cardinality/PseudoBoolean/Linear constraints. A good concept and implementation for modules. Documentation: Check which of the test suite in tests-to-port are still interesting.