mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 00:41:56 +00:00
Code Activity

remove case for non-emptiness to combine with standard membership

Browse source 
as part of revising engine for addressing #5693
This commit is contained in:
Nikolaj Bjorner 2021-12-13 18:17:40 -08:00
parent b2af7ea68f
commit f40becf099
5 changed files with 8 additions and 78 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_seq.cpp
View file

@ -3014,10 +3014,6 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
if (is_true)
m_regex.propagate_is_empty(lit);
}
else if (m_sk.is_is_non_empty(e)) {
if (is_true)
m_regex.propagate_is_non_empty(lit);
}
else if (m_sk.is_eq(e, e1, e2)) {
if (is_true) {
propagate_eq(lit, e1, e2, true);