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

wrong assert, compiler warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-10-30 10:10:54 -07:00
parent c03c395267
commit d64bc795f0
6 changed files with 1 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/seq_decl_plugin.cpp
View file

@ -1679,7 +1679,6 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
lbool nullable(l_false); lbool nullable(l_false);
unsigned min_length(0), lower_bound(0), upper_bound(UINT_MAX); unsigned min_length(0), lower_bound(0), upper_bound(UINT_MAX);
bool is_value(false); bool is_value(false);
bool normalized(false);
if (e->get_family_id() == u.get_family_id()) { if (e->get_family_id() == u.get_family_id()) {
switch (e->get_decl()->get_decl_kind()) { switch (e->get_decl()->get_decl_kind()) {
case OP_RE_EMPTY_SET: case OP_RE_EMPTY_SET:

1
src/sat/smt/arith_solver.cpp
View file

@ -911,7 +911,6 @@ namespace arith {
theory_var v = (i + start) % sz; theory_var v = (i + start) % sz;
if (is_bool(v)) if (is_bool(v))
continue; continue;
enode* n1 = var2enode(v);
ensure_column(v); ensure_column(v);
if (!can_get_ivalue(v)) if (!can_get_ivalue(v))
continue; continue;

2
src/sat/smt/bv_internalize.cpp
View file

@ -139,7 +139,7 @@ namespace bv {
n = mk_enode(e, suppress_args); n = mk_enode(e, suppress_args);
SASSERT(!n->is_attached_to(get_id())); SASSERT(!n->is_attached_to(get_id()));
theory_var v = mk_var(n); mk_var(n);
SASSERT(n->is_attached_to(get_id())); SASSERT(n->is_attached_to(get_id()));
if (internalize_mode::no_delay_i != get_internalize_mode(a)) if (internalize_mode::no_delay_i != get_internalize_mode(a))
mk_bits(n->get_th_var(get_id())); mk_bits(n->get_th_var(get_id()));

1
src/sat/smt/euf_internalize.cpp
View file

@ -21,7 +21,6 @@ Author:
namespace euf { namespace euf {
void solver::internalize(expr* e, bool redundant) { void solver::internalize(expr* e, bool redundant) {
SASSERT(!get_enode(e) || get_enode(e)->bool_var() < UINT_MAX);
if (get_enode(e)) if (get_enode(e))
return; return;
if (si.is_bool_op(e)) if (si.is_bool_op(e))

1
src/sat/smt/euf_solver.cpp
View file

@ -276,7 +276,6 @@ namespace euf {
return; return;
bool sign = l.sign(); bool sign = l.sign();
m_egraph.set_value(n, sign ? l_false : l_true); m_egraph.set_value(n, sign ? l_false : l_true);
auto const & j = s().get_justification(l);
for (auto th : enode_th_vars(n)) for (auto th : enode_th_vars(n))
m_id2solver[th.get_id()]->asserted(l); m_id2solver[th.get_id()]->asserted(l);

2
src/sat/smt/q_mbi.cpp
View file

@ -166,7 +166,6 @@ namespace q {
flatten_and(fml, result->vbody); flatten_and(fml, result->vbody);
} }
expr_ref& mbody = result->mbody; expr_ref& mbody = result->mbody;
unsigned sz = q->get_num_decls();
if (!m_model->eval_expr(q->get_expr(), mbody, true)) if (!m_model->eval_expr(q->get_expr(), mbody, true))
return nullptr; return nullptr;
@ -187,7 +186,6 @@ namespace q {
*/ */
expr_ref mbqi::basic_project(model& mdl, quantifier* q, app_ref_vector& vars) { expr_ref mbqi::basic_project(model& mdl, quantifier* q, app_ref_vector& vars) {
unsigned sz = q->get_num_decls(); unsigned sz = q->get_num_decls();
unsigned max_generation = 0;
expr_ref_vector vals(m); expr_ref_vector vals(m);
vals.resize(sz, nullptr); vals.resize(sz, nullptr);
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {