(z3str3, smt.phase_selection=1) Soundness bug on QF_S formula with str.at and str.substr

[muchang]

Hi,
For this case, Z3 gives an incorrect answer:

[572] % z3 small.smt2
unsat
[573] % z3 smt.arith.solver=2 small.smt2
unsat
[574] % z3 smt.arith.solver=2 smt.string_solver=z3str3 small.smt2
unsat
[575] % z3 smt.string_solver=z3str3 small.smt2
sat
[576] % cat small.smt2
(set-option :smt.phase_selection 1)
(declare-fun a () String)
(assert (= (str.at (str.substr (str.substr a 1 (- (str.len a) 1)) 0 (-
 (str.len (str.substr a 1 (- (str.len a) 1))) 1)) 0) "a"))
(assert (= (str.at (str.substr a 1 (- (str.len a) 1)) (- (str.len
 (str.substr a 1 (- (str.len a) 1))) 1)) "b"))
(assert (not (= (str.at (str.substr a 1 (- (str.len a) 1)) 0) "a")))
(assert (= (str.at a 0) "c"))
(check-sat)
[577] %

OS: Ubuntu 18.04
Commit: 1729232

[NikolajBjorner]

still unsound

[NikolajBjorner]

@mtrberzi - can you comment on whether issues will be addressed and/or close stale issues.