mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
parent
ec39d84f57
commit
a069b65669
|
@ -71,7 +71,7 @@ private:
|
|||
buffer<char> m_buffer;
|
||||
unsigned m_bpos;
|
||||
unsigned m_bend;
|
||||
char m_last_char;
|
||||
char m_last_char;
|
||||
bool m_is_interactive;
|
||||
bool m_smt2;
|
||||
bool m_bv_token;
|
||||
|
|
|
@ -2106,6 +2106,7 @@ namespace smt {
|
|||
enode * p = *it1;
|
||||
if (p->get_decl() == j2->m_decl &&
|
||||
m_context.is_relevant(p) &&
|
||||
p->get_num_args() > j2->m_arg_pos &&
|
||||
p->is_cgr() &&
|
||||
p->get_arg(j2->m_arg_pos)->get_root() == n) {
|
||||
// p is in joint2
|
||||
|
|
Loading…
Reference in a new issue