This will succeed with sideCondVerifierOptions, as Copilot's Abs operation is well defined precisely when C's abs function is well defined.