Hi,
For this formula:
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(assert (or (distinct a (str.++ b c)) (distinct b d)
(not (str.in.re d (str.to.re ".")))))
(check-sat)
Z3 throws out an assertion violation:
ASSERTION VIOLATION
File: ../src/util/old_buffer.h
Line: 201
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
OS: Ubuntu 18.04
Commit: 601b399
Hi,
For this formula:
Z3 throws out an assertion violation:
OS: Ubuntu 18.04
Commit: 601b399