Construct Z3 functions prior to basic constraints
Problem
Currently, Z3 functions are created on the fly when DSEML expressions are translated. This requires a certain order in the constraints passed to the Transformator. This hidden requirement already led to issues in the past when basic constraints or the AF3<->Backend interface has been adjusted.
Resolution
Create all Z3 functions when the DSEML ->Z3 transformator is created such that the existence of known Z3 functions is always guaranteed independent of the constraint order passed to the transformator.
(from redmine: issue id 3832, created on 2019-10-01)