diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp index 36b61e9a2..eb57070e8 100644 --- a/src/ast/simplifiers/solve_eqs.cpp +++ b/src/ast/simplifiers/solve_eqs.cpp @@ -317,11 +317,11 @@ namespace euf { } bool solve_eqs::is_linear(expr* t) const { - unsigned num_values = 0; if (!is_app(t)) return false; + unsigned num_values = 0; for (auto arg : *to_app(t)) - num_values += m.is_value(arg) ? 1 : 0; + if (m.is_value(arg)) ++num_values; return num_values <= 1; } diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index cfa146477..49042e3be 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -21,7 +21,7 @@ def_module_params(module_name='smt', ('elim_unconstrained', BOOL, True, 'pre-processing: eliminate unconstrained subterms'), ('solve_eqs', BOOL, True, 'pre-processing: solve equalities'), ('solve_eqs.non_ground', BOOL, True, 'pre-processing: solve equalities. Allow eliminating variables by non-ground solutions which can break behavior for model evaluation.'), - ('solve_eqs.linear', BOOL, False, 'allow only linear substitutions where a variable is replaced by a term having at most one non-constant argument'), + ('solve_eqs.linear', BOOL, False, 'allow only linear substitutions where a variable is replaced by a term having at most one non-constant argument'), ('propagate_values', BOOL, True, 'pre-processing: propagate values'), ('bound_simplifier', BOOL, True, 'apply bounds simplification during pre-processing'), ('pull_nested_quantifiers', BOOL, False, 'pre-processing: pull nested quantifiers'),