[bits 64]
adc byte [eax], 12h
adc byte [r8d], 12h
