mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix #3594

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-30 12:40:15 -07:00
parent 7936df8e0b
commit aeee44398d
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_arith_nl.h
View file

@ -794,7 +794,7 @@ bool theory_arith<Ext>::branch_nl_int_var(theory_var v) {
TRACE("non_linear", tout << "BRANCHING on v" << v << "\n";);
m_stats.m_nl_branching++;
SASSERT(is_int(v));
expr * bound = nullptr;
expr_ref bound(get_manager());
if (lower(v))
bound = m_util.mk_le(var2expr(v), m_util.mk_numeral(lower_bound(v).get_rational().to_rational(), true));
else if (upper(v))
@ -825,8 +825,7 @@ template<typename Ext>
bool theory_arith<Ext>::is_monomial_linear(expr * m) const {
SASSERT(is_pure_monomial(m));
unsigned num_nl_vars = 0;
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
expr * arg = to_app(m)->get_arg(i);
for (expr* arg : *to_app(m)) {
theory_var _var = expr2var(arg);
if (!is_fixed(_var)) {
num_nl_vars++;