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

#5215

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-27 16:02:08 -07:00
parent 4da4591fe7
commit 89373d5bf9
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/sat/smt/array_model.cpp
View file

@ -39,8 +39,10 @@ namespace array {
dep.add(n, p->get_arg(i)); dep.add(n, p->get_arg(i));
} }
for (euf::enode* k : euf::enode_class(n)) for (euf::enode* k : euf::enode_class(n))
if (a.is_const(k->get_expr())) if (a.is_const(k->get_expr()))
dep.add(n, k->get_arg(0)); dep.add(n, k->get_arg(0));
if (!dep.deps().contains(n))
dep.insert(n, nullptr);
return true; return true;
} }