Bug #73: Added one tiny branch in _to_sympy() so an AST with value '&' becomes an uninterpreted function application (we don't try to prove bitwise relations symbolically)

Author: mojtaba-eshghie

src/sindi/comparator.py

@@ -161,7 +161,9 @@ def _to_sympy_expr(self, ast):
             return base[index]
 
         args = [self._to_sympy_expr(child) for child in ast.children]
-
+        
+        if ast.value == '&' and len(args) == 2:
+            return sp.Function('BITAND')(*args)
 
         # Normalize ==/!= with boolean literals to X / !X
         if ast.value in ('==', '!=') and len(args) == 2: