mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
patch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
197aefd111
commit
370706b2b7
|
@ -2086,6 +2086,7 @@ namespace smt {
|
|||
for (; it != end; ++it) {
|
||||
enode * p = *it;
|
||||
if (p->get_decl() == f &&
|
||||
p->get_num_args() > i &&
|
||||
m_context.is_relevant(p) &&
|
||||
p->is_cgr() &&
|
||||
p->get_arg(i)->get_root() == n) {
|
||||
|
|
Loading…
Reference in a new issue