mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 09:58:59 +00:00
Code Activity

Fix duplicate ADD_SIMPLIFIER registration for purify-arith causing assertion failure

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-12 22:45:28 +00:00
parent 8c0ea9f0e7
commit a06e0193f4
1 changed files with 0 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/tactic/arith/purify_arith_tactic.h
View file

@ -78,7 +78,6 @@ tactic * mk_purify_arith_tactic(ast_manager & m, params_ref const & p = params_r
/*
ADD_TACTIC("purify-arith", "eliminate unnecessary operators: -, /, div, mod, rem, is-int, to-int, ^, root-objects.", "mk_purify_arith_tactic(m, p)")
ADD_SIMPLIFIER("purify-arith", "eliminate unnecessary operators: -, /, div, mod, rem, is-int, to-int, ^, root-objects.", "alloc(purify_arith_simplifier, m, p, s)")
*/