mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

remove useless literal found during review #5470

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-10 09:29:39 -07:00
parent 4beb29d45e
commit 2075cb9fa4
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/seq_axioms.cpp
View file

@ -1108,7 +1108,7 @@ namespace seq {
expr_ref c = m_sk.mk("seq.prefix.c", s, t, char_sort);
expr_ref d = m_sk.mk("seq.prefix.d", s, t, char_sort);
add_clause(lit, s_gt_t, mk_seq_eq(s, mk_concat(x, seq.str.mk_unit(c), y)));
add_clause(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, seq.str.mk_unit(d), z)), mk_seq_eq(t, x));
add_clause(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, seq.str.mk_unit(d), z)));
add_clause(lit, s_gt_t, ~mk_eq(c, d));
#endif
}