search

VeriFIT / z3-noodler

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

Prefix: fixing the positive case #176

Closed vhavlena closed 6 days ago

vhavlena commented 1 week ago

Results:

# of formulae: 103405
--------------------------------------------------
tool                            ✅    ❌       time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ------  ----  ---------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-0122b33-17ffaf6  102443   962   12100.47   0.12   0.02   1.66  62952    39491        528   372        62        0
z3-noodler-5249443-17ffaf6  102431   974   12179.01   0.12   0.02   1.67  62942    39489        530   380        64        0
cvc5-1.2.0                   99841  3564   73861.19   0.74   0.01   6.42  60931    38910          2  3553         9        0
z3-4.13.0                    97745  5660  128712.47   1.32   0.01   7.95  58927    38818        211  4914       465       70
--------------------------------------------------

image

jurajsic commented 1 week ago

Nice, but you should compare with z3-noodler-193f136-17ffaf6 not with z3-noodler-5249443-17ffaf6 (I forgot to push it).

However, it seems like there is still a bug somewhere else, because on the original formula QF_SLIA/2019-full_str_int/py-conbyte_z3seq/leetcode_int-validWordAbbreviation/162.smt2 it still gives incorrect model (probably also on QF_SLIA/2019-full_str_int/py-conbyte_z3seq/leetcode_int-validWordAbbreviation/36.smt2, I did not check).

vhavlena commented 1 week ago

Sure, updated results

# of formulae: 103405
--------------------------------------------------
tool                            ✅    ❌       time    avg    med    std    sat    unsat    unknown    TO    MO+ERR    other
--------------------------  ------  ----  ---------  -----  -----  -----  -----  -------  ---------  ----  --------  -------
z3-noodler-0122b33-17ffaf6  102443   962   12100.47   0.12   0.02   1.66  62952    39491        528   372        62        0
z3-noodler-193f136-17ffaf6  102442   963   12345.08   0.12   0.02   1.72  62953    39489        530   372        61        0
cvc5-1.2.0                   99841  3564   73861.19   0.74   0.01   6.42  60931    38910          2  3553         9        0
z3-4.13.0                    97745  5660  128712.47   1.32   0.01   7.95  58927    38818        211  4914       465       70
--------------------------------------------------

image