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

remove unreferenced

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-06-21 09:17:17 +02:00
parent 5177cc4a9a
commit b1dbea328a
3 changed files with 16 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/factor_equivs.cpp
View file

@ -76,7 +76,7 @@ void factor_eqs(expr_ref_vector &v, expr_equiv_class &equiv) {
*/ */
expr *choose_rep(expr_equiv_class::eq_class &clazz, ast_manager &m) { expr *choose_rep(expr_equiv_class::eq_class &clazz, ast_manager &m) {
expr *rep = nullptr; expr *rep = nullptr;
unsigned rep_sz, elem_sz; unsigned rep_sz = 0, elem_sz;
for (expr *elem : clazz) { for (expr *elem : clazz) {
if (!m.is_value(elem)) { if (!m.is_value(elem)) {
elem_sz = get_num_exprs(elem); elem_sz = get_num_exprs(elem);

1
src/parsers/smt2/smt2parser.cpp
View file

@ -3112,7 +3112,6 @@ namespace smt2 {
sexpr_ref parse_sexpr_ref() { sexpr_ref parse_sexpr_ref() {
m_num_bindings = 0; m_num_bindings = 0;
unsigned found_errors = 0;
m_num_open_paren = 0; m_num_open_paren = 0;
try { try {

29
src/sat/sat_ddfw.cpp
View file

@ -561,22 +561,23 @@ namespace sat {
IF_VERBOSE(0, if (v_reward != reward(v)) verbose_stream() << v << " " << v_reward << " " << reward(v) << "\n"); IF_VERBOSE(0, if (v_reward != reward(v)) verbose_stream() << v << " " << v_reward << " " << reward(v) << "\n");
SASSERT(reward(v) == v_reward); SASSERT(reward(v) == v_reward);
} }
for (auto const& ci : m_clauses) { DEBUG_CODE(
SASSERT(ci.m_weight > 0); for (auto const& ci : m_clauses) {
} SASSERT(ci.m_weight > 0);
for (unsigned i = 0; i < m_clauses.size(); ++i) {
bool found = false;
for (literal lit : get_clause(i)) {
if (is_true(lit)) found = true;
} }
SASSERT(found == !m_unsat.contains(i)); for (unsigned i = 0; i < m_clauses.size(); ++i) {
} bool found = false;
// every variable in a false clause is in unsat vars for (literal lit : get_clause(i)) {
for (unsigned cl : m_unsat) { if (is_true(lit)) found = true;
for (literal lit : get_clause(cl)) { }
SASSERT(m_unsat_vars.contains(lit.var())); SASSERT(found == !m_unsat.contains(i));
} }
} // every variable in a false clause is in unsat vars
for (unsigned cl : m_unsat) {
for (literal lit : get_clause(cl)) {
SASSERT(m_unsat_vars.contains(lit.var()));
}
});
} }
void ddfw::updt_params(params_ref const& _p) { void ddfw::updt_params(params_ref const& _p) {