search

VeriFIT / z3-noodler

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

Incorrect result #135

Closed jurajsic closed 2 months ago

jurajsic commented 6 months ago

We give sat on QF_SLIA/2019-full_str_int/py-conbyte_trauc/leetcode_int-numDecodings/130.smt2 for z3-noodler-3233733-2cddb2f on release version on pikachu (and everywhere else we give unknown, so it is not possible to debug). See #133

jurajsic commented 2 months ago

I do not know if the bugs in #133 and #165 are related, maybe yes, I was able to find this problematix formula:

(set-logic QF_SLIA)
(declare-fun abbr () String)
(declare-fun x4 () Int)
(declare-fun x5 () String)
(declare-fun x6 () Int)

(assert (= x4 ( str.to_int abbr  )))
(assert (= x5 
                ( str.from_int
                        x4
                )))
(assert (= x6 ( str.to_int x5
            )))

(assert (or (and ( str.prefixof "-" x5) ( = x6 1)) (and (not ( str.prefixof "-" x5))  ( = x6 0))))

(assert ( str.in_re abbr ( re.range "1" "9"  )))

(check-sat)
(get-model)
(exit)