Length Decision Procedure: models

[vhavlena]

This PR includes

• a couple of fixes in the length decision procedure
• model generation for the length procedure (including the version with shared variables)
• README update because now I feel quite confident about the model generation

[vhavlena]

Model generation vs. models turned off (on kaluza). No wrong models.

Benchmark kaluza
# of formulae: 19432
--------------------------------------------------
tool                                  ✅    ❌     time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
---------------------------------  -----  ----  -------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-model-321a050-2756940   19373    59   605.05   0.03   0.02   0.85  16278     3095         20    25         0       14
z3-noodler-length-ab1b074-2756940  19371    61   419.92   0.02   0.01   0.79  16277     3094         20    26        15        0
cvc5-1.1.2                         19431     1  1061.97   0.05   0.00   1.87  16302     3129          0     1         0        0
z3-4.13.0                          19139   293  1428.86   0.07   0.01   1.71  16022     3117          0   293         0        0
--------------------------------------------------

Comparison to devel with model generation turned off (on all benchmarks)

# of formulae: 103405
--------------------------------------------------
tool                                   ✅    ❌       time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
---------------------------------  ------  ----  ---------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-length-ab1b074-2756940  102570   835   11314.68   0.11   0.02   1.53  63084    39486        550   216        69        0
z3-noodler-ab88926-2756940         102443   962   12031.47   0.12   0.02   1.63  62955    39488        530   364        68        0
cvc5-1.1.2                          99774  3631   76479.19   0.77   0.00   6.77  60870    38904          2  3620         9        0
z3-4.13.0                           97745  5660  128712.47   1.32   0.01   7.95  58927    38818        211  4914       465       70
--------------------------------------------------

[jurajsic]

I think you can merge.