From 84b12dddac6f92b14470b8bd7c0c332550527979 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 Feb 2020 20:41:59 -0800 Subject: [PATCH] fix #3057 Signed-off-by: Nikolaj Bjorner --- src/qe/nlqsat.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index 714323c67..8a8fbf02d 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -608,7 +608,7 @@ namespace qe { if (a.is_div(n, n1, n2) && a.is_numeral(n2, r) && !r.is_zero()) { return; } - if (a.is_power(n, n1, n2) && a.is_numeral(n2, r) && r.is_unsigned()) { + if (a.is_power(n, n1, n2) && a.is_numeral(n2, r) && r.is_unsigned() && r.is_pos()) { return; } if (a.is_div(n) && s.m_mode == qsat_t && is_ground(n)) {