Finish Z3 encoding of Dcalc

[denismerigoux]

Several parts of the Z3 encoding of Dcalc are missing and should be completed:

https://github.com/CatalaLang/catala/blob/5f34fcb192a20c73786e420dd418ebdb3d069f0c/compiler/verification/z3backend.ml#L111

https://github.com/CatalaLang/catala/blob/5f34fcb192a20c73786e420dd418ebdb3d069f0c/compiler/verification/z3backend.ml#L113

https://github.com/CatalaLang/catala/blob/5f34fcb192a20c73786e420dd418ebdb3d069f0c/compiler/verification/z3backend.ml#L127

https://github.com/CatalaLang/catala/blob/5f34fcb192a20c73786e420dd418ebdb3d069f0c/compiler/verification/z3backend.ml#L147

https://github.com/CatalaLang/catala/blob/5f34fcb192a20c73786e420dd418ebdb3d069f0c/compiler/verification/z3backend.ml#L162-L164

And some others, neatly signaled by the failwith.

[R1kM]

While several components are still not or partially supported, the current encoding is sufficient to handle all variables from the "allocations_familiales" example. I'd suggest extending the current support for the missing constructs on an "on-demand" basis, i.e., when new Catala code leads to failures in the encoding.