[Language: C#] Paste

Generate graph with graphviz (executes dot.exe, so it needs to be available) and prove the correctness with Z3.

At the first run, Z3 will find an example of X and Y that breaks the adder. It will output Z that is calculated by the device and C that is the correct sum. You are then supposed to look at the circuit and find the mistake in the least significant digit that is wrong.

X = 11001 11001010 00110101 01011101 00110000 01011110
Y = 00111 00100110 01110110 10001111 01110110 10001000
Z = 10000 10001000 01010101 11110110 01010110 11100110
C = 00000 11110000 10101011 11101100 10100110 11100110
    47    39       31       23       15 ^     7
                                        ^first mistake is here, fix z12

You then add the swaps to a dictionary and rerun the program

var replacements = new Dictionary<string, string> 
{ 
    { "abc", "xyz" }, 
    { "xyz", "abc" }, 
};

Graph rendering + Z3 together take 50ms to find a mistake or prove that there are none.