z3str3 crash bug

[wintered]

Hi,

the following formula triggers a crash bug in Z3 and smt.string_solver=z3str3.

(declare-fun x () String)
(declare-fun z () Int)
(assert
 (or
  (not
   (=
    (str.replace "A" (int.to.str z) x)
    (str.++ "A" (str.replace "" (int.to.str z) x))))
  (or
   (=
    (str.replace x (str.at x z) "")
    (str.++
     (str.replace
      (str.++ (str.substr x 48 z) (str.substr x z 33))
      (str.substr x z 99)
      "")
     (str.substr x (+ 19 z) (str.len x)))))))
(check-sat)

NOT IMPLEMENTED YET!
ASSERTION VIOLATION
File: ../src/smt/theory_str.cpp
Line: 8935
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Revision: 05ad90c

[NikolajBjorner]

@mtrberzi

[NikolajBjorner]

reconciled in #2728