mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-05 19:42:23 +00:00
Code Activity

fix warnings in nra_solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-11-25 21:46:51 -08:00
parent 1c3fb49878
commit 324fb2194b
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/lp/nra_solver.cpp
View file

@ -128,7 +128,7 @@ struct solver::imp {
poly = poly * constant(den * coeff / denominators[v]);
p = p + poly;
}
auto lit = add_constraint(p, ci, k);
add_constraint(p, ci, k);
}
definitions.reset();
}
@ -295,7 +295,6 @@ struct solver::imp {
coeffs.push_back(mpz(-1));
polynomial::polynomial_ref p(pm.mk_polynomial(2, coeffs.data(), mls), pm);
auto lit = mk_literal(p.get(), lp::lconstraint_kind::EQ);
nlsat::assumption a = nullptr;
m_nlsat->mk_clause(1, &lit, nullptr);
}