mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
fix #7024
This commit is contained in:
parent
d469c1054e
commit
41a3196c89
|
@ -95,7 +95,7 @@ namespace nla {
|
|||
|
||||
scoped_anum& solver::tmp2() {
|
||||
SASSERT(use_nra_model());
|
||||
return m_core->m_nra.tmp1();
|
||||
return m_core->m_nra.tmp2();
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -918,7 +918,7 @@ namespace arith {
|
|||
theory_var v = (i + start) % sz;
|
||||
if (is_bool(v))
|
||||
continue;
|
||||
if (!ctx.is_shared(var2enode(v)) && !include_func_interp(var2enode(v)))
|
||||
if (!ctx.is_shared(var2enode(v)))
|
||||
continue;
|
||||
ensure_column(v);
|
||||
if (!is_registered_var(v))
|
||||
|
|
|
@ -1513,7 +1513,7 @@ public:
|
|||
for (theory_var i = 0; i < sz; ++i) {
|
||||
theory_var v = (i + start) % sz;
|
||||
enode* n1 = get_enode(v);
|
||||
if (!th.is_relevant_and_shared(n1) && !include_func_interp(n1))
|
||||
if (!th.is_relevant_and_shared(n1))
|
||||
continue;
|
||||
ensure_column(v);
|
||||
if (!is_registered_var(v))
|
||||
|
|
Loading…
Reference in a new issue