diff --git a/pysmt/simplifier.py b/pysmt/simplifier.py
index 418bc0d..3303577 100644
--- a/pysmt/simplifier.py
+++ b/pysmt/simplifier.py
@@ -445,7 +445,7 @@ class Simplifier(walkers.DagWalker):
                 res = args[0].bv_unsigned_value() // args[1].bv_unsigned_value()
                 res = res % 2**formula.bv_width()
             return self.manager.BV(res, width=formula.bv_width())
-        return self.manager.BVUdiv(*args)
+        return self.manager.BVUDiv(*args)
 
     def walk_bv_urem(self, formula, args):
         if args[0].is_bv_constant() and args[1].is_bv_constant:
@@ -454,7 +454,7 @@ class Simplifier(walkers.DagWalker):
             else:
                 res = args[0].bv_unsigned_value() % args[1].bv_unsigned_value()
             return self.manager.BV(res, width=formula.bv_width())
-        return self.manager.BVUrem(*args)
+        return self.manager.BVURem(*args)
 
     def walk_bv_ult(self, formula, args):
         if args[0].is_bv_constant() and args[1].is_bv_constant:
@@ -506,7 +506,7 @@ class Simplifier(walkers.DagWalker):
             filler = bitstr[0]
             res = filler*formula.bv_extend_step() + bitstr
             return self.manager.BV(res, width=formula.bv_width())
-        return self.manager.BVSext(args[0], formula.bv_extend_step())
+        return self.manager.BVSExt(args[0], formula.bv_extend_step())
 
     def walk_bv_zext(self, formula, args):
         if args[0].is_bv_constant():
@@ -517,7 +517,7 @@ class Simplifier(walkers.DagWalker):
         return self.manager.BVZExt(args[0], formula.bv_extend_step())
 
     def walk_bv_concat(self, formula, args):
-        if args[0].is_bv_constant() and args[1].is_bv_constant:
+        if args[0].is_bv_constant() and args[1].is_bv_constant():
             w0 = args[0].bv_width()
             w1 = args[1].bv_width()
             res = (2**w1) * args[0].bv_unsigned_value() + \
@@ -526,14 +526,14 @@ class Simplifier(walkers.DagWalker):
         return self.manager.BVConcat(*args)
 
     def walk_bv_lshl(self, formula, args):
-        if args[0].is_bv_constant() and args[1].is_bv_constant:
+        if args[0].is_bv_constant() and args[1].is_bv_constant():
             res = args[0].bv_unsigned_value() << args[1].bv_unsigned_value()
             w = args[0].bv_width()
             return self.manager.BV(res % (2 ** w), w)
         return self.manager.BVLShl(*args)
 
     def walk_bv_lshr(self, formula, args):
-        if args[0].is_bv_constant() and args[1].is_bv_constant:
+        if args[0].is_bv_constant() and args[1].is_bv_constant():
             res = args[0].bv_unsigned_value() >> args[1].bv_unsigned_value()
             w = args[0].bv_width()
             return self.manager.BV(res % (2 ** w), w)
diff --git a/pysmt/walkers/identitydag.py b/pysmt/walkers/identitydag.py
index 1fc1915..b422926 100644
--- a/pysmt/walkers/identitydag.py
+++ b/pysmt/walkers/identitydag.py
@@ -31,72 +31,135 @@ class IdentityDagWalker(DagWalker):
         DagWalker.__init__(self,
                            env=env,
                            invalidate_memoization=invalidate_memoization)
+        self.mgr = self.env.formula_manager
 
     def walk_symbol(self, formula, args):
-        return self.env.formula_manager.Symbol(formula.symbol_name(),
+        return self.mgr.Symbol(formula.symbol_name(),
                                                formula.symbol_type())
 
     def walk_real_constant(self, formula, args):
-        return self.env.formula_manager.Real(formula.constant_value())
+        return self.mgr.Real(formula.constant_value())
 
     def walk_int_constant(self, formula, args):
-        return self.env.formula_manager.Int(formula.constant_value())
+        return self.mgr.Int(formula.constant_value())
 
     def walk_bool_constant(self, formula, args):
-        return self.env.formula_manager.Bool(formula.constant_value())
+        return self.mgr.Bool(formula.constant_value())
 
     def walk_and(self, formula, args):
-        return self.env.formula_manager.And(args)
+        return self.mgr.And(args)
 
     def walk_or(self, formula, args):
-        return self.env.formula_manager.Or(args)
+        return self.mgr.Or(args)
 
     def walk_not(self, formula, args):
-        return self.env.formula_manager.Not(args[0])
+        return self.mgr.Not(*args)
 
     def walk_iff(self, formula, args):
-        return self.env.formula_manager.Iff(args[0], args[1])
+        return self.mgr.Iff(*args)
 
     def walk_implies(self, formula, args):
-        return self.env.formula_manager.Implies(args[0], args[1])
+        return self.mgr.Implies(*args)
 
     def walk_equals(self, formula, args):
-        return self.env.formula_manager.Equals(args[0], args[1])
+        return self.mgr.Equals(*args)
 
     def walk_ite(self, formula, args):
-        return self.env.formula_manager.Ite(args[0], args[1], args[2])
+        return self.mgr.Ite(*args)
 
     def walk_ge(self, formula, args):
-        return self.env.formula_manager.GE(args[0], args[1])
+        return self.mgr.GE(*args)
 
     def walk_le(self, formula, args):
-        return self.env.formula_manager.LE(args[0], args[1])
+        return self.mgr.LE(*args)
 
     def walk_gt(self, formula, args):
-        return self.env.formula_manager.GT(args[0], args[1])
+        return self.mgr.GT(*args)
 
     def walk_lt(self, formula, args):
-        return self.env.formula_manager.LT(args[0], args[1])
+        return self.mgr.LT(*args)
 
     def walk_forall(self, formula, args):
         qvars = [self.walk_symbol(v, None) for v in formula.quantifier_vars()]
-        return self.env.formula_manager.ForAll(qvars,args[0])
+        return self.mgr.ForAll(qvars, *args)
 
     def walk_exists(self, formula, args):
         qvars = [self.walk_symbol(v, None) for v in formula.quantifier_vars()]
-        return self.env.formula_manager.Exists(qvars,args[0])
+        return self.mgr.Exists(qvars, *args)
 
     def walk_plus(self, formula, args):
-        return self.env.formula_manager.Plus(args)
+        return self.mgr.Plus(args)
 
     def walk_times(self, formula, args):
-        return self.env.formula_manager.Times(args[0], args[1])
+        return self.mgr.Times(*args)
 
     def walk_minus(self, formula, args):
-        return self.env.formula_manager.Minus(args[0], args[1])
+        return self.mgr.Minus(*args)
 
     def walk_function(self, formula, args):
-        return self.env.formula_manager.Function(formula.function_name(), args)
+        return self.mgr.Function(formula.function_name(), args)
 
     def walk_toreal(self, formula, args):
-        return self.env.formula_manager.ToReal(args[0])
+        return self.mgr.ToReal(*args)
+
+    def walk_bv_constant(self, formula, args):
+        return self.mgr.BV(formula.constant_value(), formula.bv_width())
+
+    def walk_bv_and(self, formula, args):
+        return self.mgr.BVAnd(*args)
+
+    def walk_bv_not(self, formula, args):
+        return self.mgr.BVNot(*args)
+
+    def walk_bv_neg(self, formula, args):
+        return self.mgr.BVNeg(*args)
+
+    def walk_bv_or(self, formula, args):
+        return self.mgr.BVOr(*args)
+
+    def walk_bv_xor(self, formula, args):
+        return self.mgr.BVXor(*args)
+
+    def walk_bv_add(self, formula, args):
+        return self.mgr.BVAdd(*args)
+
+    def walk_bv_mul(self, formula, args):
+        return self.mgr.BVMul(*args)
+
+    def walk_bv_udiv(self, formula, args):
+        return self.mgr.BVUDiv(*args)
+
+    def walk_bv_urem(self, formula, args):
+        return self.mgr.BVURem(*args)
+
+    def walk_bv_ult(self, formula, args):
+        return self.mgr.BVULT(*args)
+
+    def walk_bv_ule(self, formula, args):
+        return self.mgr.BVULE(*args)
+
+    def walk_bv_extract(self, formula, args):
+        return self.mgr.BVExtract(args[0],
+                                  start=formula.bv_extract_start(),
+                                  end=formula.bv_extract_end())
+
+    def walk_bv_ror(self, formula, args):
+        return self.mgr.BVRor(args[0], formula.bv_rotation_step())
+
+    def walk_bv_rol(self, formula, args):
+        return self.mgr.BVRol(args[0], formula.bv_rotation_step())
+
+    def walk_bv_sext(self, formula, args):
+        return self.mgr.BVSExt(args[0], formula.bv_extend_step())
+
+    def walk_bv_zext(self, formula, args):
+        return self.mgr.BVZExt(args[0], formula.bv_extend_step())
+
+    def walk_bv_concat(self, formula, args):
+        return self.mgr.BVConcat(*args)
+
+    def walk_bv_lshl(self, formula, args):
+        return self.mgr.BVLShl(*args)
+
+    def walk_bv_lshr(self, formula, args):
+        return self.mgr.BVLShr(*args)

IdentityDagWalker lacks BV support
diff --git a/pysmt/test/test_walkers.py b/pysmt/test/test_walkers.py
index 22a96c7..6defb39 100644
--- a/pysmt/test/test_walkers.py
+++ b/pysmt/test/test_walkers.py
@@ -25,6 +25,7 @@ from pysmt.typing import INT, BOOL, REAL, FunctionType
 from pysmt.walkers import TreeWalker, DagWalker, IdentityDagWalker
 from pysmt.test import TestCase
 from pysmt.formula import FormulaManager
+from pysmt.test.examples import get_example_formulae
 
 from six.moves import xrange
 
@@ -100,7 +101,7 @@ class TestWalkers(TestCase):
         self.assertFalse(tree_walker.is_complete())
 
 
-    def test_identity_walker(self):
+    def test_identity_walker_simple(self):
 
         def walk_and_to_or(formula, args, **kwargs):
             return Or(args)
@@ -125,6 +126,11 @@ class TestWalkers(TestCase):
         result = walker.walk(alternation)
         self.assertEqual(result, expected)
 
+    def test_identity_dag_walker(self):
+        idw = IdentityDagWalker()
+        for (f, _, _, _) in get_example_formulae():
+            rebuilt = idw.walk(f)
+            self.assertTrue(rebuilt == f, "Rebuilt formula is not identical")
 
     def test_substitution_on_quantifiers(self):
         x, y = FreshSymbol(), FreshSymbol()

pip install -e .[dev]
parse_log_pytest
requirements.txt
nose pytest
apt-get update apt-get install -y gcc
3.9
requirements/base.txt
pytest --no-header -rA --tb=line --color=no -p no:cacheprovider -W ignore::DeprecationWarning
exceptiongroup==1.2.2
iniconfig==2.1.0
nose==1.3.7
packaging==24.2
pluggy==1.5.0
-e git+https://github.com/pysmt/pysmt.git@4fd83af49e7784a874f57620809404d530929366#egg=PySMT
pytest==8.3.5
six==1.17.0
tomli==2.2.1

name: pysmt
channels:
  - defaults
  - https://repo.anaconda.com/pkgs/main
  - https://repo.anaconda.com/pkgs/r
  - conda-forge
dependencies:
  - _libgcc_mutex=0.1=main
  - _openmp_mutex=5.1=1_gnu
  - ca-certificates=2025.2.25=h06a4308_0
  - ld_impl_linux-64=2.40=h12ee557_0
  - libffi=3.4.4=h6a678d5_1
  - libgcc-ng=11.2.0=h1234567_1
  - libgomp=11.2.0=h1234567_1
  - libstdcxx-ng=11.2.0=h1234567_1
  - ncurses=6.4=h6a678d5_0
  - openssl=3.0.16=h5eee18b_0
  - pip=25.0=py39h06a4308_0
  - python=3.9.21=he870216_1
  - readline=8.2=h5eee18b_0
  - setuptools=75.8.0=py39h06a4308_0
  - sqlite=3.45.3=h5eee18b_0
  - tk=8.6.14=h39e8969_0
  - tzdata=2025a=h04d1e81_0
  - wheel=0.45.1=py39h06a4308_0
  - xz=5.6.4=h5eee18b_1
  - zlib=1.2.13=h5eee18b_1
  - pip:
      - exceptiongroup==1.2.2
      - iniconfig==2.1.0
      - nose==1.3.7
      - packaging==24.2
      - pluggy==1.5.0
      - pytest==8.3.5
      - six==1.17.0
      - tomli==2.2.1
prefix: /opt/conda/envs/pysmt

pysmt/test/test_walkers.py::TestWalkers::test_identity_dag_walker
pysmt/test/test_walkers.py::TestWalkers::test_identity_walker_simple pysmt/test/test_walkers.py::TestWalkers::test_iterative_get_free_variables pysmt/test/test_walkers.py::TestWalkers::test_subst pysmt/test/test_walkers.py::TestWalkers::test_substituter_conditions pysmt/test/test_walkers.py::TestWalkers::test_substitution_complex pysmt/test/test_walkers.py::TestWalkers::test_substitution_on_functions pysmt/test/test_walkers.py::TestWalkers::test_substitution_on_quantifiers pysmt/test/test_walkers.py::TestWalkers::test_substitution_term pysmt/test/test_walkers.py::TestWalkers::test_undefined_node pysmt/test/test_walkers.py::TestWalkers::test_walker_is_complete
pysmt/walkers/identitydag.py pysmt/simplifier.py
pysmt/walkers/identitydag.py pysmt/simplifier.py