mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

Fix #7505 (#7565)

Browse source 
* fix #7505

* rename
This commit is contained in:
Hari Govind V K 2025-02-20 17:54:59 +00:00 • committed by GitHub
parent bd3d288a08
commit f50f21198e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/qe/mbp/mbp_dt_tg.cpp
View file

@ -72,11 +72,11 @@ struct mbp_dt_tg::impl {
// rewrite head(x) with y
// and x with list(y, z)
void rm_select(expr *term) {
void rm_accessor(expr *term) {
SASSERT(is_app(term) &&
m_dt_util.is_accessor(to_app(term)->get_decl()) &&
is_var(to_app(term)->get_arg(0)));
TRACE("mbp_tg", tout << "applying rm_select on " << expr_ref(term, m););
has_var(to_app(term)->get_arg(0)));
TRACE("mbp_tg", tout << "applying rm_accessor on " << expr_ref(term, m););
expr *v = to_app(term)->get_arg(0);
expr_ref sel(m);
app_ref u(m);
@ -162,10 +162,10 @@ struct mbp_dt_tg::impl {
if (m_tg.is_cgr(term)) continue;
if (is_app(term) &&
m_dt_util.is_accessor(to_app(term)->get_decl()) &&
is_var(to_app(term)->get_arg(0))) {
has_var(to_app(term)->get_arg(0))) {
mark_seen(term);
progress = true;
rm_select(term);
rm_accessor(term);
continue;
}
if (is_constructor_app(term, cons, rhs)) {