Assertion violation at src/ast/ast.cpp:431

[wintered]

[530] % z3release small.smt2
sat
[531] % z3release smt.string_solver=z3str3 small.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 431
UNREACHABLE CODE WAS REACHED.
Z3 4.8.9.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[532] % 
[532] % cat small.smt2
(set-option :smt.str.fixed_length_naive_cex false)
(declare-fun s () String)
(assert (not (= (str.at (str.substr s 0 (- (str.len s) 1)) 0) (str.at s 0) "a")))
(check-sat)
[533] %

OS: Ubuntu 18.04
Commit: 32055a3

[mtrberzi]

Taking a look, but the code path that's run with smt.str.fixed_length_naive_cex=false is known to have issues, which is why it's not the default.

[mtrberzi]

Fixed in 04ac5f0