On the following formula z3str3 smt.string_solver=z3str3 throws the below assertion violation.
(set-option :proof true)
(declare-fun a () String)
(declare-fun b () String)
(assert (str.contains (str.++ a b) (str.++ b "x")))
(check-sat)
ASSERTION VIOLATION
File: ../src/smt/smt_clause.cpp
Line: 45
!m.proofs_enabled() || js != 0
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
OS: Ubuntu 18.04
Commit: 9f6a0a0
On the following formula z3str3
smt.string_solver=z3str3throws the below assertion violation.OS: Ubuntu 18.04
Commit: 9f6a0a0