mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #2943

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-09 15:48:53 -08:00
parent 82273da630
commit bc75e08a52
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_arith_nl.h
View file

@ -166,6 +166,8 @@ std::pair<unsigned, int> theory_arith<Ext>::analyze_monomial(expr * m) const {
int idx = 0; int idx = 0;
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
expr * arg = to_app(m)->get_arg(i); expr * arg = to_app(m)->get_arg(i);
if (m_util.is_numeral(arg))
continue;
if (var == nullptr) { if (var == nullptr) {
var = arg; var = arg;
power = 1; power = 1;