mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

fix memory leak in SAT solver exposed by regression tests

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-06 11:47:45 -08:00
parent aec5a38b14
commit 00f3a1fe81
2 changed files with 0 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/sat/sat_solver.cpp
View file

@ -461,7 +461,6 @@ namespace sat {
} }
void solver::dettach_clause(clause & c) { void solver::dettach_clause(clause & c) {
TRACE("sat", tout << c.id() << "\n";);
if (c.size() == 3) if (c.size() == 3)
dettach_ter_clause(c); dettach_ter_clause(c);
else else

2
src/smt/theory_arith_aux.h
View file

@ -618,10 +618,8 @@ namespace smt {
template<typename Ext> template<typename Ext>
void theory_arith<Ext>::remove_fixed_vars_from_base() { void theory_arith<Ext>::remove_fixed_vars_from_base() {
int num = get_num_vars(); int num = get_num_vars();
//std::cout << "num vars " << num << "\n";
for (theory_var v = 0; v < num; v++) { for (theory_var v = 0; v < num; v++) {
if (is_base(v) && is_fixed(v)) { if (is_base(v) && is_fixed(v)) {
//std::cout << "fixed base " << v << " \n"; // << mk_pp(get_enode(v)->get_owner(), get_manager()) << "\n";
row const & r = m_rows[get_var_row(v)]; row const & r = m_rows[get_var_row(v)];
typename vector<row_entry>::const_iterator it = r.begin_entries(); typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries(); typename vector<row_entry>::const_iterator end = r.end_entries();