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

fix #5197 fix #5193

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-20 10:16:44 -07:00
parent 44d77a978a
commit b658934bd8
1 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/theory_seq.cpp
View file

@ -1872,11 +1872,14 @@ public:
app* theory_seq::get_ite_value(expr* e) {
expr* e1, *e2, *e3;
while (m.is_ite(e, e1, e2, e3)) {
if (get_root(e2) == get_root(e)) {
while (m.is_ite(e, e1, e2, e3)) {
if (!ctx.e_internalized(e))
break;
enode* r = ctx.get_enode(e)->get_root();
if (ctx.get_enode(e2)->get_root() == r) {
e = e2;
}
else if (get_root(e3) == get_root(e)) {
else if (ctx.get_enode(e3)->get_root() == r) {
e = e3;
}
else {