I'll write down an algorithm that solves SAT in time N^k if any algorithm does.

On SAT instances of size T, enumerate all algorithms of size up to log(T); for each one, consider all SAT instances of size up to log(T); run each algorithm for time log(T)^k, outputing 0 if they don't halt, and compare its output to the result of a brute force search.

Take the shortest algorithm which worked in each of these tests, and use it to answer your original SAT query of size T (aborting and outputing 0 if it takes more than T^k time).

This entire process takes time poly(T). Moreover, suppose there is an N^k time algorithm which solves SAT correctly and let A be the shortest such algorithm. Then there is a finite constant T0 such that all shorter algorithms than A fail on some SAT instance of size at most T0. Then the algorithm I described works correctly for all SAT instances of size at least 2^(T0 + |A|).

(Edit: this argument is silly; you can just run all programs of size log(T) and output a solution if any of them find one)

Edit: Note in particular that the algorithm which takes k = BB(10^10) and does a brute force search instead for T < BB(10^10) is guaranteed to solve SAT in poly time, provided that any algorithm does. Realistically, I think taking k = 10 and doing a brute for search for T < 10^10^10 is virtually guaranteed to solve SAT in poly time, if any algorithm does (and I can actually write down this latter algorithm).