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

fix #6876

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-25 17:14:35 -07:00
parent e8929041b8
commit 63467f9dfa
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -76,6 +76,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
bool m_ignore_patterns_on_ground_qbody = true;
bool m_rewrite_patterns = true;
bool m_enable_der = true;
bool m_nested_der = false;
ast_manager & m() const { return m_b_rw.m(); }
@ -92,6 +93,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
m_ignore_patterns_on_ground_qbody = p.ignore_patterns_on_ground_qbody();
m_rewrite_patterns = p.rewrite_patterns();
m_enable_der = p.enable_der();
m_nested_der = _p.get_bool("nested_der", false);
}
void updt_params(params_ref const & p) {
@ -843,8 +845,11 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
result = r;
}
if (der_change) {
if (der_change && !m_nested_der) {
th_rewriter rw(m());
params_ref p;
p.set_bool("nested_der", true);
rw.updt_params(p);
rw(result, r, p2);
if (m().proofs_enabled() && result.get() != r.get())
result_pr = m().mk_transitivity(result_pr, p2);