mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

fix #3689

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-02 11:33:22 -07:00
parent a7aff1bcf0
commit 700ad1f2b9
1 changed files with 12 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/smt/theory_arith_nl.h
View file

@ -71,9 +71,11 @@ void theory_arith<Ext>::mark_dependents(theory_var v, svector<theory_var> & vars
expr * n = var2expr(v); expr * n = var2expr(v);
SASSERT(m_util.is_mul(n)); SASSERT(m_util.is_mul(n));
for (expr * curr : *to_app(n)) { for (expr * curr : *to_app(n)) {
theory_var v = expr2var(curr); if (get_context().e_internalized(curr)) {
SASSERT(v != null_theory_var); theory_var v = expr2var(curr);
mark_var(v, vars, already_found); SASSERT(v != null_theory_var);
mark_var(v, vars, already_found);
}
} }
} }
if (is_fixed(v)) if (is_fixed(v))
@ -1122,6 +1124,8 @@ bool theory_arith<Ext>::propagate_linear_monomials() {
template<typename Ext> template<typename Ext>
bool theory_arith<Ext>::is_problematic_non_linear_row(row const & r) { bool theory_arith<Ext>::is_problematic_non_linear_row(row const & r) {
m_tmp_var_set.reset(); m_tmp_var_set.reset();
if (!reflection_enabled())
return false;
typename vector<row_entry>::const_iterator it = r.begin_entries(); typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries(); typename vector<row_entry>::const_iterator end = r.end_entries();
for (; it != end; ++it) { for (; it != end; ++it) {
@ -2380,9 +2384,11 @@ bool theory_arith<Ext>::max_min_nl_vars() {
expr * n = var2expr(v); expr * n = var2expr(v);
SASSERT(is_pure_monomial(n)); SASSERT(is_pure_monomial(n));
for (expr * curr : *to_app(n)) { for (expr * curr : *to_app(n)) {
theory_var v = expr2var(curr); if (get_context().e_internalized(curr)) {
SASSERT(v != null_theory_var); theory_var v = expr2var(curr);
mark_var(v, vars, already_found); SASSERT(v != null_theory_var);
mark_var(v, vars, already_found);
}
} }
} }
return max_min(vars); return max_min(vars);