From f7cc68aa6aabf4e997700c4599fcbe488c4c15c9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 24 Sep 2019 08:58:36 -0700 Subject: [PATCH] fix #2580 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_nl.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 1293b4546..14824c59e 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -1537,7 +1537,7 @@ namespace smt { rational a, b; unsigned n = UINT_MAX; unsigned nm = UINT_MAX; - if (in_monovariate_monomials(p, var, i1, a, n, i2, b, nm)) { + if (in_monovariate_monomials(p, var, i1, a, n, i2, b, nm) && n != nm) { CTRACE("in_monovariate_monomials", n == nm, for (unsigned i = 0; i < p.size(); i++) { if (i > 0) tout << " + "; tout << p[i].first << "*" << mk_pp(p[i].second, get_manager());