3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00

remove todo from str api

This commit is contained in:
Murphy Berzish 2017-02-17 13:28:52 -05:00
parent 2e27e1cd36
commit 90705cfd5f

View file

@ -81,7 +81,6 @@ extern "C" {
MK_UNARY(Z3_mk_str_length, mk_c(c)->get_str_fid(), OP_STRLEN, SKIP);
MK_BINARY(Z3_mk_str_at, mk_c(c)->get_str_fid(), OP_STR_CHARAT, SKIP);
// translate prefixof/suffixof to StartsWith/EndsWith
// TODO string standardization might just remove StartsWith/EndsWith in future
Z3_ast Z3_API Z3_mk_str_prefixof(Z3_context c, Z3_ast pre, Z3_ast full) {
LOG_Z3_mk_str_prefixof(c, pre, full);
Z3_TRY;