mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

fix #4330

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-05-15 08:54:40 -07:00
parent 6d96f96cc3
commit c4204d3365
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_pb.cpp
View file

@ -513,7 +513,7 @@ namespace smt {
return true; return true;
} }
ineq* c = alloc(ineq, m_mpz_mgr, literal(abv), pb.is_eq(atom)); scoped_ptr<ineq> c = alloc(ineq, m_mpz_mgr, literal(abv), pb.is_eq(atom));
c->m_args[0].m_k = pb.get_k(atom); c->m_args[0].m_k = pb.get_k(atom);
numeral& k = c->m_args[0].m_k; numeral& k = c->m_args[0].m_k;
arg_t& args = c->m_args[0]; arg_t& args = c->m_args[0];
@ -554,7 +554,6 @@ namespace smt {
// fall-through // fall-through
case l_true: case l_true:
ctx.mk_th_axiom(get_id(), 1, &lit); ctx.mk_th_axiom(get_id(), 1, &lit);
dealloc(c);
return true; return true;
case l_undef: case l_undef:
break; break;
@ -584,7 +583,7 @@ namespace smt {
init_watch_ineq(*c); init_watch_ineq(*c);
init_watch(abv); init_watch(abv);
m_var_infos[abv].m_ineq = c; m_var_infos[abv].m_ineq = c.detach();
m_ineqs_trail.push_back(abv); m_ineqs_trail.push_back(abv);
TRACE("pb", display(tout, *c);); TRACE("pb", display(tout, *c););
return true; return true;