From f9b6e4e24779968c10baf4dac952b075136abae0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 6 Oct 2019 15:25:33 -0700 Subject: [PATCH] batch length enforcement Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 615f135ed..c8a3c002e 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1904,16 +1904,25 @@ bool theory_seq::check_length_coherence() { return true; } } - for (expr* l : m_length) { + bool change = false; + unsigned sz = m_length.size(); + for (unsigned i = 0; i < sz; ++i) { + expr* l = m_length.get(i); expr* e = nullptr; VERIFY(m_util.str.is_length(l, e)); if (check_length_coherence(e)) { return true; } + enode* n = ensure_enode(e); + enode* r = n->get_root(); + if (r != n && has_length(r->get_owner())) { + continue; + } if (add_length_to_eqc(e)) { - return true; + change = true; } } + return change; } bool theory_seq::fixed_length(bool is_zero) {