Axioms are true by definition; that's what "axiom" means. (They might also be false, but (if and) only if your system is inconsistent.)
> Case (1) that machine doesn't really halt
This is not a state of affairs: all you know at any given time is that the machine hasn't halted yet (after some specific finite number of steps), or that it has aquired some termination-precluding invariant like a infinite loop (which you can detect only strictly less than all of).
Regardless, the particular technical definition of truth I'm using is Tarski's definition of truth[1]. We don't have to agree whether Tarski's definition is "correct", and I'm happy to qualify my use of the word "truth" here, but I'm referring to a specific technical definition here.
[1] https://en.wikipedia.org/wiki/Semantic_theory_of_truth#Tarsk...
So again, we have a proof in some sketchy axiom system that the machine that searches for an inconsistency in ZFC halts. The question is whether that conclusion is a true statement or not, whether that machine actually does or does not halt. You can start up that program on your laptop while we consider it. Maybe it will halt during our discussion. I also want to point out that whether that conclusion is a true statement or not has no bearing on whether the deduction system was sound to begin with. Unsound systems can prove true statement, simply by accident rather than by design.
Case (1) that machine doesn't really halt, then ZFC+¬Con(ZFC) proves an untrue statement, and we thus the system is unsound.
Case (2) that machine does really halt. Then this particular conclusion wasn't untrue, but we have another problem. We can take the output of that machine, decode it, and we have a proof of an inconsistency in ZFC. Again this is just a deduction, it doesn't mean that math is wrong or the world ends. Just that the ZFC axiom system is so unsound that it is inconsistent, and it has some untrue axioms. Nevertheless we can use such a proof and derive a proof that ZFC prove `while(true)` halts, and in turn transform that into a proof in ZFC+¬Con(ZFC) that `while(true)` halts. And it is definitely the case that `while(true)` doesn't halt. So in this case we have found a different but still untrue statement that ZFC+¬Con(ZFC) proves. Our conclusion is the same: ZFC+¬Con(ZFC) is unsound.
So in either case `ZFC+¬Con(ZFC)` proves some machine halts that doesn't. I haven't concluded which of the two machines it is wrong about though I have my personal suspicions, but it is definitely wrong about one of them.