mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 16:27:37 +00:00
Code Activity

Fix FPA soundness issue: reset rewriter cache in pop_scope_eh (issue #8345)

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-21 03:35:47 +00:00
parent b16e142127
commit 46daa160ed
1 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_fpa.cpp
View file

@ -414,6 +414,12 @@ namespace smt {
void theory_fpa::pop_scope_eh(unsigned num_scopes) {
m_trail_stack.pop_scope(num_scopes);
TRACE(t_fpa, tout << "pop " << num_scopes << "; now " << m_trail_stack.get_num_scopes() << "\n";);
// Reset the fpa2bv rewriter cache so that expressions re-converted after
// a pop regenerate their side conditions (extra_assertions). Without this,
// the rewriter returns cached results without invoking mk_uf/mk_const and
// the axioms connecting FP UFs to their BV counterparts are never re-emitted,
// causing a soundness issue in incremental mode.
m_rw.reset();
theory::pop_scope_eh(num_scopes);
}