mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

compiler warning fix

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-02-02 19:26:51 -08:00
parent efbecb19b1
commit 741634b703
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/nla_powers.cpp
View file

@ -131,7 +131,7 @@ namespace nla {
return l_false;
}
if (xval >= 3 && yval != 0 & rval <= yval + 1) {
if (xval >= 3 && yval != 0 && rval <= yval + 1) {
new_lemma lemma(c, "x >= 3, y != 0 => x^y > ln(x)y + 1");
lemma |= ineq(x, llc::LT, rational(3));
lemma |= ineq(y, llc::EQ, rational::zero());