mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

fix memory leak

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-05-01 10:07:37 -07:00
parent 1ef4354080
commit 869643a551
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/nlsat/nlsat_solver.cpp
View file

@ -3033,7 +3033,7 @@ namespace nlsat {
var x, ptr_vector<clause>& clauses,
vector<bound_constraint>& lo, vector<bound_constraint>& hi) {
polynomial_ref C(m_pm);
polynomial_ref C(m_pm), D(m_pm);
for (auto c : clauses)
c->set_removed();
@ -3043,7 +3043,8 @@ namespace nlsat {
// h.A * x + h.B, h.is_strict; h.A > 0
// (l.A x + l.B)*h.A + (h.A x + h.B)*|l.A| >= 0
C = m_pm.mul(l.B, h.A);
C = m_pm.sub(C, m_pm.mul(h.B, l.A));
D = m_pm.mul(h.B, l.A);
C = m_pm.sub(C, D);
poly* p = C.get();
bool is_even = false;
m_lemma.reset();
@ -3101,6 +3102,7 @@ namespace nlsat {
auto a1 = static_cast<_assumption_set>(l.c->assumptions());
auto a2 = static_cast<_assumption_set>(h.c->assumptions());
a1 = m_asm.mk_join(a1, a2);
m_lemma_assumptions = a1;
// TODO: this can also replace solve_eqs
for (auto c : clauses) {