From dc7c94a3acf0f0f014fc6f9e36a240113a516cd6 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Wed, 27 May 2026 17:37:39 +0200 Subject: [PATCH] le != lt --- src/smt/seq/seq_nielsen.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 0691d6a8e..beeaeae0f 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -1251,6 +1251,10 @@ namespace seq { seq_util& seq = this->graph().seq(); bool changed = true; + if (id() == 4) { + graph().to_dot(std::cout); + std::flush(std::cout); + } // DON'T add rules here that add new constraints or apply substitutions // add them to apply_det_modifier instead @@ -4458,7 +4462,7 @@ namespace seq { nielsen_node* child = mk_child(node); nielsen_edge* e = mk_edge(node, child, true); child->m_str_deq.pop_back(); - expr_ref cmp(this->a.mk_le(u_len, v_len), m); + expr_ref cmp(this->a.mk_lt(u_len, v_len), m); m_rw(cmp); e->add_side_constraint(constraint(cmp, first.m_dep, m)); } @@ -4467,7 +4471,7 @@ namespace seq { nielsen_node* child = mk_child(node); nielsen_edge* e = mk_edge(node, child, true); child->m_str_deq.pop_back(); - expr_ref cmp(this->a.mk_le(v_len, u_len), m); + expr_ref cmp(this->a.mk_lt(v_len, u_len), m); m_rw(cmp); e->add_side_constraint(constraint(cmp, first.m_dep, m)); }