mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix unsoundness bug instroduced when fixing #1125

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-06-30 19:36:38 -07:00
parent c44c8284bd
commit be4b0ffe69
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_seq.cpp
View file

@ -2879,7 +2879,9 @@ expr_ref theory_seq::try_expand(expr* e, dependency*& eqs){
expr_ref result(m);
expr_dep ed;
if (m_rep.find_cache(e, ed)) {
eqs = m_dm.mk_join(eqs, ed.second);
if (e != ed.first) {
eqs = m_dm.mk_join(eqs, ed.second);
}
result = ed.first;
}
else {
@ -2889,9 +2891,9 @@ expr_ref theory_seq::try_expand(expr* e, dependency*& eqs){
}
expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) {
expr_ref result(m);
dependency* deps = 0;
result = try_expand(e0, deps);
result = try_expand(e0, eqs);
if (result) return result;
dependency* deps = 0;
expr* e = m_rep.find(e0, deps);
expr* e1, *e2, *e3;
expr_ref arg1(m), arg2(m);