From a06e0193f4e568bfcc559373200d17c2d8a02e12 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 12 Mar 2026 22:45:28 +0000
Subject: [PATCH] Fix duplicate ADD_SIMPLIFIER registration for purify-arith
 causing assertion failure

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/tactic/arith/purify_arith_tactic.h | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/tactic/arith/purify_arith_tactic.h b/src/tactic/arith/purify_arith_tactic.h
index 7303a2791..f65fa2cac 100644
--- a/src/tactic/arith/purify_arith_tactic.h
+++ b/src/tactic/arith/purify_arith_tactic.h
@@ -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)")
 */