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

integrate some self-contained fixes from #2147

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-24 14:21:34 -08:00
parent 142f3638cf
commit 6ef3e5e363
2 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/substitution/substitution.cpp
View file

@ -112,7 +112,7 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e
TRACE("subst_bug", tout << "visited: " << visited << ", n1: " << mk_pp(n1.get_expr(), m_manager) << " : " << n1.get_offset() << "\n";);
if (visited) {
m_todo.pop_back();
expr * new_expr;
expr * new_expr = nullptr;
m_apply_cache.find(n1, new_expr);
m_apply_cache.insert(n, new_expr);
TRACE("subst_bug", tout << "1. insert n: " << mk_pp(n.get_expr(), m_manager) << " : " << n.get_offset()

2
src/util/array.h
View file

@ -151,7 +151,7 @@ public:
if (m_data == nullptr) {
return 0;
}
return static_cast<unsigned>(reinterpret_cast<size_t *>(m_data)[SIZE_IDX]);
return static_cast<unsigned>(reinterpret_cast<size_t *>(m_data)[ARRAY_SIZE_IDX]);
}
bool empty() const { return m_data == nullptr; }