Convert many examples to java backend

**do not review yet**
It is OK with me to let it pass in order to speed up the removal of Maude, but at least we should add a task for this to be fixed asap after the removal of Maude.  It is quite unnatural to get the SMT involved here.