Missed rewrite str.replace_all?

Z3Prover / z3

The Z3 Theorem Prover

Other

10.42k stars 1.47k forks source link

Missed rewrite str.replace_all? #5344

Closed wintered closed 3 years ago

wintered commented 3 years ago

Commit: 082ec0f OS: Ubuntu 18.04

[548] % z3release small.smt2
""
(str.replace_all "" (str.++ s "A") s)
[549] % cvc5 -q small.smt2
""
(str.replace_all "" (str.++ s "A") s)
[550] % cat small.smt2
(declare-fun s () String)
(simplify (str.replace "" (str.++ s "A") s))
(simplify (str.replace_all "" (str.++ s "A") s))
[551] %

NikolajBjorner commented 3 years ago

replace_all is parsed but not supported with inferences