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

removing warnings for unused variables, #579

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-05-17 16:02:08 -07:00
parent 09b8c0e7fa
commit cc3bfe8da2
3 changed files with 6 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/qi_queue.cpp
View file

@ -377,11 +377,10 @@ namespace smt {
bool result = true;
for (unsigned i = 0; i < sz; i++) {
entry & e = m_delayed_entries[i];
fingerprint * f = e.m_qb;
TRACE("qi_queue", tout << f << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";);
TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";);
if (!e.m_instantiated && e.m_cost <= min_cost) {
TRACE("qi_queue",
tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast<quantifier*>(f->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";);
tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast<quantifier*>(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";);
result = false;
m_instantiated_trail.push_back(i);
m_stats.m_num_lazy_instances++;
@ -394,11 +393,10 @@ namespace smt {
bool result = true;
for (unsigned i = 0; i < m_delayed_entries.size(); i++) {
entry & e = m_delayed_entries[i];
fingerprint * f = e.m_qb;
TRACE("qi_queue", tout << f << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";);
TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";);
if (!e.m_instantiated && e.m_cost <= m_params.m_qi_lazy_threshold) {
TRACE("qi_queue",
tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast<quantifier*>(f->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";);
tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast<quantifier*>(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";);
result = false;
m_instantiated_trail.push_back(i);
m_stats.m_num_lazy_instances++;

3
src/smt/smt_model_finder.cpp
View file

@ -3545,10 +3545,9 @@ namespace smt {
//
// Since we only care about q (and its bindings), it only makes sense to restrict the variables of q.
bool asserted_something = false;
quantifier * flat_q = get_flat_quantifier(q);
unsigned num_decls = q->get_num_decls();
// Remark: sks were created for the flat version of q.
SASSERT(flat_q->get_num_decls() == sks.size());
SASSERT(get_flat_quantifier(q)->get_num_decls() == sks.size());
SASSERT(sks.size() >= num_decls);
for (unsigned i = 0; i < num_decls; i++) {
expr * sk = sks.get(num_decls - i - 1);

3
src/smt/theory_seq.cpp
View file

@ -3741,7 +3741,6 @@ expr_ref theory_seq::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned
rej(s, idx, re, i) -> len(s) > idx if i is final
*/
void theory_seq::propagate_acc_rej_length(literal lit, expr* e) {
context& ctx = get_context();
expr *s, * idx, *re;
unsigned src;
eautomaton* aut = 0;
@ -3752,7 +3751,7 @@ void theory_seq::propagate_acc_rej_length(literal lit, expr* e) {
}
if (m_util.str.is_length(idx)) return;
SASSERT(m_autil.is_numeral(idx));
SASSERT(ctx.get_assignment(lit) == l_true);
SASSERT(get_context().get_assignment(lit) == l_true);
bool is_final = aut->is_final_state(src);
if (is_final == is_acc) {
propagate_lit(0, 1, &lit, mk_literal(m_autil.mk_ge(m_util.str.mk_length(s), idx)));