mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-08 19:35:25 +00:00
Code Activity

Prevent unsound solve-eqs elimination across recursive-function definitions (#9358)

Browse source 
* Initial plan

* Prevent unsound solve-eqs elimination across recursive-function definitions

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/9a2fc92f-15e8-4806-988b-28bce96e8007

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Update solve_eqs.cpp

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Copilot 2026-04-23 16:17:21 +02:00 • committed by GitHub
parent abd378e9d8
commit 99f64b80fa
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 23 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/simplifiers/solve_eqs.cpp
View file

@ -244,10 +244,17 @@ namespace euf {
unsigned count = 0;
vector<dependent_expr> old_fmls;
dep_eq_vector eqs;
struct reset_unsafe {
solve_eqs& s;
reset_unsafe(solve_eqs& s): s(s) {}
~reset_unsafe() { s.m_unsafe_vars.reset(); }
};
reset_unsafe ru(*this);
do {
old_fmls.reset();
m_subst_ids.reset();
eqs.reset();
filter_unsafe_vars();
get_eqs(eqs);
extract_dep_graph(eqs);
extract_subst();
@ -265,6 +272,7 @@ namespace euf {
old_fmls.reset();
m_subst_ids.reset();
eqs.reset();
filter_unsafe_vars();
solve_context_eqs context_solve(*this);
context_solve.collect_nested_equalities(eqs);
extract_dep_graph(eqs);
@ -334,7 +342,7 @@ namespace euf {
m_unsafe_vars.reset();
recfun::util rec(m);
for (func_decl* f : rec.get_rec_funs())
for (expr* term : subterms::all(expr_ref(rec.get_def(f).get_rhs(), m), &m_todo, &m_visited))
for (expr* term : subterms::all(expr_ref(rec.get_def(f).get_rhs(), m)))
m_unsafe_vars.mark(term);
}

14
src/test/fpa.cpp
View file

@ -60,6 +60,20 @@ static void test_fp_to_real_denormal() {
true);
}
static void test_recfun_defined_function_soundness() {
run_fp_test(
"(set-option :model_validate true)\n"
"(declare-fun fixedAdd () Int)\n"
"(declare-fun variableAdd () Int)\n"
"(define-fun-rec $$add$$ ((a Int) (b Int)) Int\n"
" (ite (= 0 b) 2 (- a (+ 0 (- fixedAdd b)))))\n"
"(assert (= fixedAdd (* 9 fixedAdd)))\n"
"(assert (= 1 ($$add$$ 1 3)))\n"
"(check-sat)\n",
false);
}
void tst_fpa() {
test_fp_to_real_denormal();
test_recfun_defined_function_soundness();
}