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

fix regression with uninitialized variable

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-09-23 15:51:26 -05:00
parent c41b6da6bb
commit 6226875283
3 changed files with 4 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -98,6 +98,7 @@ namespace arith {
void solver::found_underspecified(expr* n) { void solver::found_underspecified(expr* n) {
if (a.is_underspecified(n)) { if (a.is_underspecified(n)) {
TRACE("arith", tout << "Unhandled: " << mk_pp(n, m) << "\n";); TRACE("arith", tout << "Unhandled: " << mk_pp(n, m) << "\n";);
ctx.push(push_back_vector(m_underspecified));
m_underspecified.push_back(to_app(n)); m_underspecified.push_back(to_app(n));
} }
expr* e = nullptr, * x = nullptr, * y = nullptr; expr* e = nullptr, * x = nullptr, * y = nullptr;
@ -243,6 +244,7 @@ namespace arith {
mk_abs_axiom(t); mk_abs_axiom(t);
else if (a.is_idiv(n, n1, n2)) { else if (a.is_idiv(n, n1, n2)) {
if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n); if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);
ctx.push(push_back_vector(m_idiv_terms));
m_idiv_terms.push_back(n); m_idiv_terms.push_back(n);
app_ref mod(a.mk_mod(n1, n2), m); app_ref mod(a.mk_mod(n1, n2), m);
internalize(mod, m_is_redundant); internalize(mod, m_is_redundant);

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

@ -681,10 +681,7 @@ namespace arith {
scope& sc = m_scopes.back(); scope& sc = m_scopes.back();
sc.m_bounds_lim = m_bounds_trail.size(); sc.m_bounds_lim = m_bounds_trail.size();
sc.m_asserted_qhead = m_asserted_qhead; sc.m_asserted_qhead = m_asserted_qhead;
sc.m_idiv_lim = m_idiv_terms.size();
sc.m_asserted_lim = m_asserted.size(); sc.m_asserted_lim = m_asserted.size();
sc.m_not_handled = m_not_handled;
sc.m_underspecified_lim = m_underspecified.size();
lp().push(); lp().push();
if (m_nla) if (m_nla)
m_nla->push(); m_nla->push();
@ -696,11 +693,8 @@ namespace arith {
TRACE("arith", tout << "pop " << num_scopes << "\n";); TRACE("arith", tout << "pop " << num_scopes << "\n";);
unsigned old_size = m_scopes.size() - num_scopes; unsigned old_size = m_scopes.size() - num_scopes;
del_bounds(m_scopes[old_size].m_bounds_lim); del_bounds(m_scopes[old_size].m_bounds_lim);
m_idiv_terms.shrink(m_scopes[old_size].m_idiv_lim);
m_asserted.shrink(m_scopes[old_size].m_asserted_lim); m_asserted.shrink(m_scopes[old_size].m_asserted_lim);
m_asserted_qhead = m_scopes[old_size].m_asserted_qhead; m_asserted_qhead = m_scopes[old_size].m_asserted_qhead;
m_underspecified.shrink(m_scopes[old_size].m_underspecified_lim);
m_not_handled = m_scopes[old_size].m_not_handled;
m_scopes.resize(old_size); m_scopes.resize(old_size);
lp().pop(num_scopes); lp().pop(num_scopes);
m_new_bounds.reset(); m_new_bounds.reset();
@ -1117,7 +1111,7 @@ namespace arith {
if (m_delayed_eqs.empty()) if (m_delayed_eqs.empty())
return true; return true;
force_push(); force_push();
for (unsigned i; i < m_delayed_eqs.size(); ++i) { for (unsigned i = 0; i < m_delayed_eqs.size(); ++i) {
auto p = m_delayed_eqs[i]; auto p = m_delayed_eqs[i];
auto const& e = p.first; auto const& e = p.first;
if (p.second) if (p.second)

5
src/sat/smt/arith_solver.h
View file

@ -105,11 +105,8 @@ namespace arith {
struct scope { struct scope {
unsigned m_bounds_lim; unsigned m_bounds_lim;
unsigned m_idiv_lim;
unsigned m_asserted_qhead; unsigned m_asserted_qhead;
unsigned m_asserted_lim; unsigned m_asserted_lim;
unsigned m_underspecified_lim;
expr* m_not_handled;
}; };
class resource_limit : public lp::lp_resource_limit { class resource_limit : public lp::lp_resource_limit {
@ -220,7 +217,7 @@ namespace arith {
svector<std::pair<euf::th_eq, bool>> m_delayed_eqs; svector<std::pair<euf::th_eq, bool>> m_delayed_eqs;
literal_vector m_asserted; literal_vector m_asserted;
expr* m_not_handled{ nullptr }; expr* m_not_handled = nullptr;
ptr_vector<app> m_underspecified; ptr_vector<app> m_underspecified;
ptr_vector<expr> m_idiv_terms; ptr_vector<expr> m_idiv_terms;
vector<ptr_vector<api_bound> > m_use_list; // bounds where variables are used. vector<ptr_vector<api_bound> > m_use_list; // bounds where variables are used.