mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-05 06:46:11 +00:00
Code Activity

le != lt

Browse source
This commit is contained in:
CEisenhofer 2026-05-27 17:37:39 +02:00
parent b7f9019a6e
commit dc7c94a3ac
1 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/seq/seq_nielsen.cpp
View file

@ -1251,6 +1251,10 @@ namespace seq {
seq_util& seq = this->graph().seq(); seq_util& seq = this->graph().seq();
bool changed = true; 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 // DON'T add rules here that add new constraints or apply substitutions
// add them to apply_det_modifier instead // add them to apply_det_modifier instead
@ -4458,7 +4462,7 @@ namespace seq {
nielsen_node* child = mk_child(node); nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true); nielsen_edge* e = mk_edge(node, child, true);
child->m_str_deq.pop_back(); 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); m_rw(cmp);
e->add_side_constraint(constraint(cmp, first.m_dep, m)); e->add_side_constraint(constraint(cmp, first.m_dep, m));
} }
@ -4467,7 +4471,7 @@ namespace seq {
nielsen_node* child = mk_child(node); nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true); nielsen_edge* e = mk_edge(node, child, true);
child->m_str_deq.pop_back(); 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); m_rw(cmp);
e->add_side_constraint(constraint(cmp, first.m_dep, m)); e->add_side_constraint(constraint(cmp, first.m_dep, m));
} }