mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

fix #2913

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-03 09:14:23 -08:00
parent fc4c1dac25
commit 47cdb5f46e
1 changed files with 7 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/smt/theory_arith_nl.h
View file

@ -1225,24 +1225,19 @@ bool theory_arith<Ext>::get_polynomial_info(sbuffer<coeff_expr> const & p, sbuff
for (auto const& ce : p) { for (auto const& ce : p) {
expr * m = ce.second; expr * m = ce.second;
if (is_pure_monomial(m)) { if (m_util.is_numeral(m)) {
continue;
}
else if (ctx.e_internalized(m) && !is_pure_monomial(m)) {
ADD_OCC(m);
}
else {
unsigned num_vars = get_num_vars_in_monomial(m); unsigned num_vars = get_num_vars_in_monomial(m);
for (unsigned i = 0; i < num_vars; i++) { for (unsigned i = 0; i < num_vars; i++) {
var_power_pair p = get_var_and_degree(m, i); var_power_pair p = get_var_and_degree(m, i);
ADD_OCC(p.first); ADD_OCC(p.first);
} }
} }
else if (m_util.is_numeral(m)) {
continue;
}
else if (ctx.e_internalized(m)) {
ADD_OCC(m);
}
else {
TRACE("non_linear", tout << mk_pp(m, get_manager()) << "\n";);
UNREACHABLE();
return false;
}
} }
// Update the number of occurrences in the result vector. // Update the number of occurrences in the result vector.