(unicode=false smt.arith.eager_eq_axioms=false) Solution unsoundness on QF_S formula

[muchang]

[585] % z3release small.smt2
unsat
[586] % z3release unicode=false small.smt2
unsat
[587] % z3release unicode=false smt.arith.eager_eq_axioms=false small.smt2
sat
[588] % cat small.smt2
(declare-fun a () String)
(assert (= (ite (str.suffixof "-" (str.at a 1)) 0 (str.to_code (str.at a 1))) 0))
(assert (ite (str.suffixof "-" (str.at a 1)) true (not (= 0 (str.to_int (str.at a 1))))))
(assert (str.in_re (str.at a 1) (re.+ (re.range "0" "9"))))
(check-sat)
[589] %

Commit: 1da7522

[NikolajBjorner]

can't take parameter fuzz bugs like these on seq