Hi,
For this formula:
(assert (= "" (str.replace_all "" "" "")))
(check-sat)
Z3 throws out an assertion violation:
ASSERTION VIOLATION
File: ../src/ast/seq_decl_plugin.cpp
Line: 919
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
OS: Ubuntu 18.04
Commit: fc8dfe3
Hi,
For this formula:
Z3 throws out an assertion violation:
OS: Ubuntu 18.04
Commit: fc8dfe3