[Z3Backend] Add support for enumerations containing argument-less constructors

[R1kM]

This PR adds Z3 encoding support for elements of type TUnit, which are generated as arguments of enumeration constructors that do not have any argument in Catala.
Values of type unit are encoded to Z3 as a tuple with 0 elements.
The unit value and type are generated once and for all when initializing the global context for simplicity, since it should be the same everywhere.
Simple unit tests for absence of errors, presence of an empty error and presence of an exception overlap were also added to tests/test_proof

[R1kM]

The addition of this functionality was leading to failures when trying to run the proof platform on examples/allocations_familiales/allocations_familiales.catala_fr. The root cause was that, when trying to retrieve a model for a function, print_model was using Model.get_const_interp, which apparently throws an (undocumented) exception when the corresponding Z3 declaration is not a constant expr but a function.
To avoid this error, I added the logic for correctly retrieving the Z3 model of a Catala function, and used Z3 built-ins facilities to print this model during counterexample generation. Pretty-printing these functions will be addressed in a future PR.

[denismerigoux]

Looks perfect, I'm merging!