mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
4532b07e88
commit
52df98f9ca
|
@ -644,8 +644,6 @@ bool array_rewriter::add_store(expr_ref_vector& args, unsigned num_idxs, expr* e
|
|||
bool array_rewriter::is_expandable_store(expr* s) {
|
||||
unsigned count = 0;
|
||||
unsigned depth = 0;
|
||||
if (false && !is_ground(s))
|
||||
return false;
|
||||
while (m_util.is_store(s)) {
|
||||
s = to_app(s)->get_arg(0);
|
||||
count += s->get_ref_count();
|
||||
|
|
|
@ -597,6 +597,7 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
|
|||
end_scope();
|
||||
cache_result<ProofGen>(q, m_r, m_pr, fr.m_cache_result);
|
||||
m_r = nullptr;
|
||||
m_pr = nullptr;
|
||||
frame_stack().pop_back();
|
||||
set_new_child_flag(q, m_r);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue