Dear everyone in the academia (and maybe elsewhere) doing #bindiffing research: #SymbolicExecution does not work for comparing different architectures, unless you are using as input for your symbolic execution tool *decompiled code*.

If you are using assembly or using an IR (Intermediate Representation) based on assembler (like Ghidra' p-code, IDA's microcode, LLVM's IR, etc), it will inevitably produce different outputs.

Your best IR for #diffing is pseudo-code, the #decompiler's output.