(seq and z3str) Issues in string solvers

[rainoftime]

Hi, for the following formula

(set-logic QF_SLIA)
(declare-const i7 Int)
(declare-const Str3 String)
(declare-const Str7 String)
(declare-const Str14 String)
(assert (str.in_re Str14 (str.to_re (str.substr Str14 0 (abs i7)))))
(assert (str.in_re (str.++ Str3 "pprtut" Str7 "") (re.++ (str.to_re (str.substr Str14 0 (abs i7))) (str.to_re "qbtciigmtwadmbzhrwrpusydtnouwhnukkdarqzjmqmwcitojz"))))
(check-sat)

cvc4 yields sat, but both z3seq and z3str3 return unsat (commit 79aa3457c1)

A model given by cvc4

(model
(define-fun i7 () Int 6)
(define-fun Str3 () String "")
(define-fun Str7 () String "qbtciigmtwadmbzhrwrpusydtnouwhnukkdarqzjmqmwcitojz")
(define-fun Str14 () String "pprtut")
)

[mtrberzi]

@NikolajBjorner if this is affecting both string solvers, maybe something is going on with seq_rewriter? I can take a look today if it's useful.

[rainoftime]

At commit db65381f3

(set-logic QF_S)
(declare-const Str11 String)
(assert (str.in_re (str.++ "" "wyeuem" "" "mpzyyy" Str11) (re.opt (str.to_re Str11))))
(check-sat)

cvc4 returns unsat, but z3seq gives sat. The model given by z3 seems wrong

(model 
  (define-fun Str11 () String
    "")
)

[rainoftime]

z3str3 invalid model at 4682b48d3a

(set-logic QF_SLIA)
(set-option :model_validate true)
(set-option :smt.arith.solver 2)
(set-option :smt.string_solver z3str3)
(declare-const i7 Int)
(declare-const Str9 String)
(declare-const Str11 String)
(declare-const Str12 String)
(declare-const Str13 String)
(declare-const Str19 String)
(assert (>= (str.len Str12) 37))
(assert (= Str13 Str11 Str19 Str12 (str.substr Str9 0 i7)))
(check-sat)

sat
(error "line 13 column 10: an invalid model was generated")
(model 
  (define-fun i7 () Int
    (- 1))
  (define-fun Str9 () String
    "?????????????????????????????????????")
  (define-fun Str13 () String
    "")
  (define-fun Str11 () String
    "")
  (define-fun Str19 () String
    "")
  (define-fun Str12 () String
    "")
)

[rainoftime]

At 4682b48

(set-logic QF_S)
(set-option :smt.phase_selection 1)
(declare-const v3 Bool)
(declare-const v6 Bool)
(declare-const v11 Bool)
(declare-const Str0 String)
(declare-const Str7 String)
(declare-const Str8 String)
(declare-const Str9 String)
(declare-const Str10 String)
(declare-const Str14 String)
(declare-const Str16 String)
(declare-const Str18 String)
(assert (xor v11 true (= Str9 Str18 Str14 Str7 Str0) v11 true true true true true))
(declare-const v19 Bool)
(assert-soft (=> (= v6 (= Str10 Str8 Str16 Str0) v3) v19))
(check-sat)

ASSERTION VIOLATION
File: ../src/smt/smt_justification.cpp
Line: 311
eqs[i].first->get_root() == eqs[i].second->get_root()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

At 4682b48

(set-logic QF_SLIA)
(set-option :smt.string_solver z3str3)
(declare-const i1 Int)
(declare-const Str14 String)
(assert (>= (str.len (str.substr Str14 0 i1)) 0))
(minimize 14)
(check-sat)

ASSERTION VIOLATION
File: ../src/smt/theory_str_mc.cpp
Line: 868
lhs_chars.size() == rhs_chars.size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

z3str3 invalid model at 4682b48

(set-logic QF_SLIA)
(declare-fun _substvar_12_ () Int)
(set-option :model_validate true)
(set-option :smt.random_seed 9)
(set-option :smt.string_solver z3str3)
(declare-const Str4 String)
(assert (>= (str.len (str.substr Str4 0 _substvar_12_)) 9))
(check-sat)

sat
(error "line 8 column 10: an invalid model was generated")
(model 
  (define-fun Str4 () String
    "?????????")
  (define-fun _substvar_12_ () Int
    (- 1))
)

[rainoftime]

At commit 2d52367368c

(set-logic QF_SLIA)
(set-option :smt.string_solver z3str3)
(declare-const v4 Bool)
(declare-const i2 Int)
(declare-const Str18 String)
(assert-soft v4)
(assert (>= (str.len (str.substr Str18 0 i2)) 0))
(check-sat)

ASSERTION VIOLATION
File: ../src/smt/theory_str_mc.cpp
Line: 868
lhs_chars.size() == rhs_chars.size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

At commit 2d52367

(set-logic QF_SLIA)
(set-option :model_validate true)
(set-option :smt.arith.solver 2)
(set-option :smt.string_solver z3str3)
(declare-const i9 Int)
(declare-const Str12 String)
(assert (>= (str.len (str.substr Str12 0 i9)) 60))
(check-sat)

sat
(error "line 8 column 10: an invalid model was generated")
(model 
  (define-fun i9 () Int
    (- 1))
  (define-fun Str12 () String
    "????????????????????????????????????????????????????????????")
)