mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

perf for #4655

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-12-07 21:34:57 -08:00
parent f5f980fa38
commit c49d39af81
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_seq.cpp
View file

@ -1548,6 +1548,10 @@ void theory_seq::add_length(expr* e, expr* l) {
Add length limit restrictions to sequence s. Add length limit restrictions to sequence s.
*/ */
void theory_seq::add_length_limit(expr* s, unsigned k, bool is_searching) { void theory_seq::add_length_limit(expr* s, unsigned k, bool is_searching) {
if (m_sk.is_indexof_left(s))
return;
if (m_sk.is_indexof_right(s))
return;
#if 0 #if 0
if (m_sk.is_skolem(s)) if (m_sk.is_skolem(s))
return; return;