diff --git a/pysmt/oracles.py b/pysmt/oracles.py
index 36b8b12..5cae510 100644
--- a/pysmt/oracles.py
+++ b/pysmt/oracles.py
@@ -389,6 +389,7 @@ class AtomsOracle(walkers.DagWalker):
     # - ITE terms
     # - Symbols
     # - Constants
+    # - Array select, e.g. a[x] because such term could be of Boolean type
     #
 
     def get_atoms(self, formula):
@@ -406,11 +407,17 @@ class AtomsOracle(walkers.DagWalker):
         #pylint: disable=unused-argument
         return frozenset([formula])
 
-    @walkers.handles(op.THEORY_OPERATORS)
+    @walkers.handles(op.THEORY_OPERATORS - {op.ARRAY_SELECT})
     def walk_theory_op(self, formula, **kwargs):
         #pylint: disable=unused-argument
         return None
 
+    def walk_array_select(self, formula, **kwargs):
+        #pylint: disable=unused-argument
+        if self.env.stc.get_type(formula).is_bool_type():
+            return frozenset([formula])
+        return None
+
     @walkers.handles(op.CONSTANTS)
     def walk_constant(self, formula, **kwargs):
         #pylint: disable=unused-argument

`get_atoms()` crashes with boolean-typed arrays
There is a bug in `get_atoms()` when boolean arrays are involved.

Consider the following code:
```python
from pysmt.shortcuts import *

a = Symbol("a", ArrayType(INT, BOOL))
x = Symbol("x", INT)
p = Symbol("p", BOOL)

phi = And(Iff(Select(a, x), p), GT(x, Int(1)))

print(phi.get_atoms())
```

The current master crashes with 
```
Traceback (most recent call last):
  File "bugo.py", line 9, in <module>
    print(phi.get_atoms())
  File "/home/amicheli/work/code/pysmt/pysmt/fnode.py", line 118, in get_atoms
    return _env().ao.get_atoms(self)
  File "/home/amicheli/work/code/pysmt/pysmt/oracles.py", line 396, in get_atoms
    return self.walk(formula)
  File "/home/amicheli/work/code/pysmt/pysmt/walkers/dag.py", line 106, in walk
    res = self.iter_walk(formula, **kwargs)
  File "/home/amicheli/work/code/pysmt/pysmt/walkers/dag.py", line 98, in iter_walk
    self._process_stack(**kwargs)
  File "/home/amicheli/work/code/pysmt/pysmt/walkers/dag.py", line 91, in _process_stack
    self._compute_node_result(formula, **kwargs)
  File "/home/amicheli/work/code/pysmt/pysmt/walkers/dag.py", line 75, in _compute_node_result
    self.memoization[key] = f(formula, args=args, **kwargs)
  File "/home/amicheli/work/code/pysmt/pysmt/oracles.py", line 403, in walk_bool_op
    return frozenset(x for a in args for x in a)
  File "/home/amicheli/work/code/pysmt/pysmt/oracles.py", line 403, in <genexpr>
    return frozenset(x for a in args for x in a)
TypeError: 'NoneType' object is not iterable
```

the expected behavior is to return the set `{p, a[x], x>1}`

Thanks to Gianluca Redondi for signaling the issue.

diff --git a/pysmt/test/test_regressions.py b/pysmt/test/test_regressions.py
index 29985f8..d894eaa 100644
--- a/pysmt/test/test_regressions.py
+++ b/pysmt/test/test_regressions.py
@@ -544,6 +544,20 @@ class TestRegressions(TestCase):
         f = get_formula_strict(cStringIO(smt_script))
         self.assertSat(f, solver_name='yices')
 
+    def test_get_atoms_array_select(self):
+        a = Symbol("a", ArrayType(INT, BOOL))
+        x = Symbol("x", INT)
+        p = Symbol("p", BOOL)
+
+        phi = And(Iff(Select(a, x), p), Equals(x, Int(1)))
+
+        atoms = phi.get_atoms()
+
+        self.assertEqual(len(atoms), 3)
+        self.assertIn(Select(a, x), atoms)
+        self.assertIn(p, atoms)
+        self.assertIn(Equals(x, Int(1)), atoms)
+
 
 if __name__ == "__main__":
     main()

pip install -e .[dev]
parse_log_pytest
requirements.txt
pytest
apt-get update apt-get install -y gcc
3.9
dev-requirements.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@bc3a5f8ae22c490016a4ce98df10b7f79ac40324#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_regressions.py::TestRegressions::test_get_atoms_array_select
pysmt/test/test_regressions.py::TestRegressions::test_array_initialization_printing pysmt/test/test_regressions.py::TestRegressions::test_cnf_as_set pysmt/test/test_regressions.py::TestRegressions::test_dependencies_not_includes_toreal pysmt/test/test_regressions.py::TestRegressions::test_determinism pysmt/test/test_regressions.py::TestRegressions::test_empty_string_symbol pysmt/test/test_regressions.py::TestRegressions::test_equality_typing pysmt/test/test_regressions.py::TestRegressions::test_exactly_one_unpacking pysmt/test/test_regressions.py::TestRegressions::test_exactlyone_w_generator pysmt/test/test_regressions.py::TestRegressions::test_function_smtlib_print pysmt/test/test_regressions.py::TestRegressions::test_infix_notation_wrong_le pysmt/test/test_regressions.py::TestRegressions::test_is_one pysmt/test/test_regressions.py::TestRegressions::test_multiple_declaration_w_same_functiontype pysmt/test/test_regressions.py::TestRegressions::test_multiple_exit pysmt/test/test_regressions.py::TestRegressions::test_parse_bvconst_width pysmt/test/test_regressions.py::TestRegressions::test_parse_bvx_var pysmt/test/test_regressions.py::TestRegressions::test_parse_declare_const pysmt/test/test_regressions.py::TestRegressions::test_parse_define_fun pysmt/test/test_regressions.py::TestRegressions::test_parse_define_fun_bind pysmt/test/test_regressions.py::TestRegressions::test_parse_exception pysmt/test/test_regressions.py::TestRegressions::test_pysmt_syntax_error pysmt/test/test_regressions.py::TestRegressions::test_qf_bool_smt2 pysmt/test/test_regressions.py::TestRegressions::test_simplify_times pysmt/test/test_regressions.py::TestRegressions::test_simplifying_int_plus_changes_type_of_expression pysmt/test/test_regressions.py::TestRegressions::test_smtlib_define_fun_serialization pysmt/test/test_regressions.py::TestRegressions::test_smtlib_info_quoting pysmt/test/test_regressions.py::TestRegressions::test_string_constant_quote_escaping_hr_printer pysmt/test/test_regressions.py::TestRegressions::test_string_constant_quote_escaping_parsing pysmt/test/test_regressions.py::TestRegressions::test_string_constant_quote_escaping_smtlib_printer pysmt/test/test_regressions.py::TestRegressions::test_substitute_memoization pysmt/test/test_regressions.py::TestRegressions::test_substitute_to_real
pysmt/oracles.py
pysmt/oracles.py