Soundness bug in z3str3

[wintered]

Hi,

The following formula triggers a soundness bug in z3str3.

(declare-fun a () String)
(declare-fun b () String)
(declare-fun e () String)
(declare-fun h () String)
(declare-fun k () String)
(declare-fun l () String)
(declare-fun m () String)
(declare-fun q () String)
(declare-fun ah () String)
(declare-fun c () Bool)
(declare-fun d () Bool)
(declare-fun f () Bool)
(declare-fun g () Bool)
(declare-fun i () Bool)
(declare-fun j () Bool)
(declare-fun n () Bool)
(declare-fun ag () Bool)
(assert (= "" (str.substr a 3 (str.len e))))
(assert (= (= "" (str.substr a 0 0)) (= j d)))
(assert
 (=
  (or n (= g (= f c)))
  (and
   (= (str.substr h 4 (str.len a)) (str.++ m q))
   (str.in.re m
    (re.++ (str.to.re "")
     (re.++ (str.to.re "_")
      (re.++ (str.to.re "u")
       (re.++ (str.to.re "t")
        (re.++ (str.to.re "m")
         (re.++ (str.to.re "a")
          (re.++ (str.to.re "=")
           (re.++ (str.to.re "1")
            (re.++ (str.to.re "6")
             (re.++ (str.to.re "8")
              (str.to.re "8") (str.to.re "")))))))))))))))
(assert (= n
         (=
          (str.substr b (str.len l)
           (str.len
            (str.substr k (str.len m)
             (str.len (str.substr e (str.len q) (str.len ah)))))) "")))
(assert (= b (str.++ m ah)))
(assert (= (= c i) (not ag)))
(check-sat)

z3 smt.string_solver=z3str3 gives unsat on this formula while CVC4 and z3 (without z3str3 enabled) give sat.

Revision: 1281964
OS: Ubuntu 18.904

[NikolajBjorner]

@mtrberzi

[NikolajBjorner]

Hi,

on the following formula z3str3 using z3 smt.string_solver=z3str3 model_validate=true gives unsat while without the model_validate=true returns sat on it.

(declare-fun RrCnv_new () Bool)
(declare-fun bjvRH_new () Bool)
(declare-fun DOxcm_new () Bool)
(declare-fun wlGYz_new () Bool)
(declare-fun Wadrq_new () Bool)
(declare-fun QEKUW_new () Bool)
(declare-fun QWKkD_new () Bool)
(declare-fun b () Bool)
(declare-fun TWhvf_new () Bool)
(declare-fun xoDNP_new () Bool)
(declare-fun bHPCR_new () Bool)
(declare-fun poJbv_new () Bool)
(declare-fun bZrcp_new () Bool)
(declare-fun fBQJl_new () Bool)
(declare-fun hsNXV_new () String)
(declare-fun T_1 () Bool)
(declare-fun T_2 () Bool)
(declare-fun T_3 () Bool)
(declare-fun T_4 () Bool)
(declare-fun T_5 () Bool)
(declare-fun T_6 () Bool)
(declare-fun T_7 () Bool)
(declare-fun T_8 () Bool)
(declare-fun T_9 () Bool)
(declare-fun a () Bool)
(declare-fun T_b () Bool)
(declare-fun T_c () Bool)
(declare-fun T_d () Bool)
(declare-fun T_e () Bool)
(declare-fun var_0xINPUT_166177 () String)
(declare-fun shifted_T_1 () Bool)
(declare-fun shifted_T_2 () Bool)
(declare-fun shifted_var_0xINPUT_40408 () String)
(assert (distinct (or (distinct RrCnv_new (not (distinct bjvRH_new T_2)))) (not (distinct "" (str.substr hsNXV_new 242 (str.len var_0xINPUT_166177))))))
(assert T_1)
(assert (distinct T_2 (not (distinct "" var_0xINPUT_166177))))
(assert T_2)
(assert (distinct T_3 (and (distinct "" var_0xINPUT_166177))))
(assert (not (distinct DOxcm_new (or (= QWKkD_new T_7)) (distinct (str.substr hsNXV_new 108 (str.len var_0xINPUT_166177)) ""))))
(assert (and (distinct wlGYz_new (not (= Wadrq_new T_5)))))
(assert (distinct (and (distinct Wadrq_new (not (distinct TWhvf_new T_9)))) (distinct (str.substr hsNXV_new 130 (str.len var_0xINPUT_166177)) "")))
(assert (distinct (or (distinct QEKUW_new (or (distinct QWKkD_new T_7)))) (or T_5)))
(assert (or (distinct QEKUW_new (and (distinct QWKkD_new T_7)))))
(assert (= T_7 (and (distinct "" (str.substr hsNXV_new 71 (str.len var_0xINPUT_166177))))))
(assert T_7)
(assert (distinct T_8 (and (distinct "ywUN4ZIDAC" (str.substr hsNXV_new 247 (str.len var_0xINPUT_166177))))))
(assert (distinct T_9 (not T_8)))
(assert T_9)
(assert (distinct a (and (distinct var_0xINPUT_166177 "ywUN4ZIDAC"))))
(assert (distinct (or (= bHPCR_new (or (distinct fBQJl_new T_e)))) (and a)))
(assert (or (distinct bHPCR_new shifted_T_1)))
(assert (distinct T_c (= (str.substr hsNXV_new 214 (str.len var_0xINPUT_166177)) "")))
(assert (distinct (and (distinct bZrcp_new (or (distinct fBQJl_new T_e)))) (or T_c)))
(assert (or (distinct bZrcp_new shifted_T_1)))
(assert (distinct (or (= fBQJl_new shifted_T_1)) (not (distinct (str.substr hsNXV_new 234 (str.len var_0xINPUT_166177)) ""))))
(assert T_e)
(assert (distinct (or (distinct RrCnv_new T_1)) (or (distinct "" (str.substr hsNXV_new (str.len var_0xINPUT_166177) (str.len shifted_var_0xINPUT_40408))))))
(assert (distinct (distinct DOxcm_new T_3) (distinct RrCnv_new T_1)))
(assert (distinct DOxcm_new T_3))
(check-sat)
(get-model)

OS: Ubuntu 18.04
Revision: a257ec0