(proof=true, z3str3) Assertion violation ../src/smt/smt_context.cpp Line: 2954

[muchang]

Hi, For this formula:

(set-option :proof true)
(declare-fun a () String)
(assert (= (str.replace "B" (str.replace "" a "A") "") (str.replace "B" a "")))
(check-sat)

Z3 smt.string_solver=z3str3 throws out an assertion violation:

ASSERTION VIOLATION
File: ../src/smt/smt_context.cpp
Line: 2954
!m_all_th_case_split_literals.contains(l.index())
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

This crashes at the same location as https://github.com/Z3Prover/z3/issues/4348, but the code paths (and the formulas) seem different.

OS: Ubuntu 18.04 Commit: 0f8f886

[muchang]

Here is another case:

[553] % z3debug small.smt2
sat
[554] % z3debug smt.string_solver=z3str3 small.smt2
ASSERTION VIOLATION
File: ../src/smt/smt_context.cpp
Line: 2954
!m_all_th_case_split_literals.contains(l.index())
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[555] % 
[555] % cat small.smt2
(set-option :smt.theory_case_split true)
(declare-fun value2 () String)
(assert (not (= (ite (str.contains (str.++ (str.replace (str.substr
 (str.substr value2 0 (- (- (str.len value2)))) 0 (- (+ (str.indexof
 (str.substr value2 0 (- (- (str.len value2) 1) 0)) "P" 0) 1) 0)) "P"
 "p")) "Z") 1 0) 0)))
(check-sat)
[556] %

Changing the variable to somewhat, for example to 's' or even just 'value1', the assertion violation isn't triggered anymore.