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 #6590

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-02-15 08:36:01 -08:00
parent c2fe76569f
commit 8ce0c56ff5
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/math/lp/nla_powers.cpp
View file

@ -81,6 +81,8 @@ namespace nla {
lbool powers::check(lpvar r, lpvar x, lpvar y, vector<lemma>& lemmas) { lbool powers::check(lpvar r, lpvar x, lpvar y, vector<lemma>& lemmas) {
if (x == null_lpvar || y == null_lpvar || r == null_lpvar) if (x == null_lpvar || y == null_lpvar || r == null_lpvar)
return l_undef; 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; core& c = m_core;
if (c.use_nra_model()) if (c.use_nra_model())