Find a pushdown automaton for { x#y ∣ x ≠ y }
Since you have a marker $\#$ separating $x$ and $y$, the solution is
rather easy. The PDA must first decide non-deterministically whether
it will attempt to check that $|x|\neq|y|$ or whether $x$ and $y$
differ for their $i$-th symbol, i.e. whether $x_i\neq y_i$. This
corresponds to two distinct sets of states.

The first case can be dealt with as you suggest.

In the second case, the automaton scans the input, and stores a symbol
$a$ in its stack to keep count. At the $i$-th symbol, chosen
non-deterministically, it decides to check whether that is the symbol
rank for which $x_i\neq y_i$. So it memorizes the synbol $x_i$ in its
finite control (meaning that the states now used have a component
indicating whether a $0$ or a $1$ was found). Then, the PDA scans the
input without memorizing anything until it scans the symbol $\#$. Then
it start scanning the $y$ part, popping the stack for each symbol
read. When the stack is empty, it is reading the symbol $y_i$, and it
can check whether it is different from $x_i$ memorized in the finite
control. If it is different, the PDA can accept the string, and does
not even need to scan the rest.

If the end of the string is reached before the stack is empty, the
automaton can accept too, though this can also be handled by the first
case.