mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

fix #4187

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-05-02 11:42:03 -07:00
parent 47fa6ba7a6
commit f3dd58d7ad
2 changed files with 10 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/rewriter/rewriter.cpp
View file

@ -18,6 +18,7 @@ Notes:
--*/ --*/
#include "ast/rewriter/rewriter_def.h" #include "ast/rewriter/rewriter_def.h"
#include "ast/ast_ll_pp.h" #include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
#include "ast/ast_smt2_pp.h" #include "ast/ast_smt2_pp.h"
void rewriter_core::init_cache_stack() { void rewriter_core::init_cache_stack() {
@ -47,6 +48,9 @@ bool rewriter_core::rewrites_from(expr* t, proof* p) {
} }
bool rewriter_core::rewrites_to(expr* t, proof* p) { bool rewriter_core::rewrites_to(expr* t, proof* p) {
CTRACE("rewriter", p && !m().proofs_disabled() && to_app(m().get_fact(p))->get_arg(1) != t,
tout << mk_pp(p, m()) << "\n";
tout << mk_pp(t, m()) << "\n";);
return !p || m().proofs_disabled() || (to_app(m().get_fact(p))->get_arg(1) == t); return !p || m().proofs_disabled() || (to_app(m().get_fact(p))->get_arg(1) == t);
} }
@ -76,6 +80,8 @@ void rewriter_core::cache_shifted_result(expr * k, unsigned offset, expr * v) {
void rewriter_core::cache_result(expr * k, expr * v, proof * pr) { void rewriter_core::cache_result(expr * k, expr * v, proof * pr) {
m_cache->insert(k, v); m_cache->insert(k, v);
SASSERT(m_proof_gen); SASSERT(m_proof_gen);
SASSERT(rewrites_from(k, pr));
SASSERT(rewrites_to(v, pr));
m_cache_pr->insert(k, pr); m_cache_pr->insert(k, pr);
} }

7
src/ast/rewriter/th_rewriter.cpp
View file

@ -698,11 +698,12 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
p1 = m().mk_pull_quant(old_q, q1); p1 = m().mk_pull_quant(old_q, q1);
} }
} }
else if ( else if (old_q->get_kind() == lambda_k &&
old_q->get_kind() == lambda_k &&
is_ground(new_body)) { is_ground(new_body)) {
result = m_ar_rw.util().mk_const_array(old_q->get_sort(), new_body); result = m_ar_rw.util().mk_const_array(old_q->get_sort(), new_body);
result_pr = nullptr; if (m().proofs_enabled()) {
result_pr = m().mk_rewrite(old_q, result);
}
return true; return true;
} }
else { else {