mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-06 09:00:52 +00:00
Code Activity

Cleanup thanks to Copilot (#9709)

Browse source
This commit is contained in:
Hari Govind V K 2026-06-04 18:46:33 +01:00 • committed by GitHub
parent 400fe313d9
commit 98ce7f5d05
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -166,15 +166,14 @@ struct mbp_dt_tg::impl {
// Only apply rm_accessor if the model confirms the argument // Only apply rm_accessor if the model confirms the argument
// has the constructor that this accessor belongs to. // has the constructor that this accessor belongs to.
// Otherwise we introduce a contradictory is-cons literal. // Otherwise we introduce a contradictory is-cons literal.
func_decl *cons = func_decl *acc_cons =
m_dt_util.get_accessor_constructor(to_app(term)->get_decl()); m_dt_util.get_accessor_constructor(to_app(term)->get_decl());
func_decl *rec = m_dt_util.get_constructor_recognizer(cons); func_decl *rec = m_dt_util.get_constructor_recognizer(acc_cons);
expr_ref is_rec(m.mk_app(rec, to_app(term)->get_arg(0)), m); expr_ref is_rec(m.mk_app(rec, to_app(term)->get_arg(0)), m);
if (!m_mdl.is_true(is_rec)) { if (!m_mdl.is_true(is_rec)) {
// Ground the argument so the accessor term becomes // The accessor's argument does not have the expected constructor in the model.
// constructively ground. This preserves any enclosing // Add a guard literal and skip rm_accessor so we don't force a contradictory
// literal (e.g., (not (is-nil (tl nil)))) as a guard in // constructor constraint on the argument.
// the output, preventing an over-approximation.
expr_ref is(m.mk_not(is_rec), m); expr_ref is(m.mk_not(is_rec), m);
m_tg.add_lit(is); m_tg.add_lit(is);
mark_seen(term); mark_seen(term);

1
src/test/mbp_qel.cpp
View file

@ -239,6 +239,7 @@ static void test_dt_multiple_vars() {
VERIFY(!m.is_false(projected)); VERIFY(!m.is_false(projected));
VERIFY(mdl->is_true(projected)); VERIFY(mdl->is_true(projected));
VERIFY(vars.empty());
std::cout << " PASS\n\n"; std::cout << " PASS\n\n";
} }