search

VeriFIT / z3-noodler

The Z3-Noodler String Solver
Other
6 stars 5 forks source link

Models for unary decision procedure #161

Closed vhavlena closed 1 month ago

vhavlena commented 1 month ago

Adding decision procedure for unary systems with the corresponding model generation module.

vhavlena commented 1 month ago

Results are ok

# of formulae: 103405
--------------------------------------------------
tool                            ✅    ❌       time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ------  ----  ---------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-8bca24a-7c3f5d0  102393  1012   11555.10   0.11   0.02   1.53  62907    39486        537   406        69        0
z3-noodler-9dacadd-bdcb62d  102393  1012   11618.30   0.11   0.02   1.53  62911    39482        537   409        66        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
--------------------------------------------------

image