From 8ce0c56ff5580e199c7c940b49419e792582786b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Feb 2023 08:36:01 -0800 Subject: [PATCH] fix #6590 --- src/math/lp/nla_powers.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/math/lp/nla_powers.cpp b/src/math/lp/nla_powers.cpp index 3af31a48816..96284f26a77 100644 --- a/src/math/lp/nla_powers.cpp +++ b/src/math/lp/nla_powers.cpp @@ -81,6 +81,8 @@ namespace nla { lbool powers::check(lpvar r, lpvar x, lpvar y, vector& lemmas) { if (x == null_lpvar || y == null_lpvar || r == null_lpvar) return l_undef; + if (lp::tv::is_term(x) || lp::tv::is_term(y) || lp::tv::is_term(r)) + return l_undef; core& c = m_core; if (c.use_nra_model())