SAT solvers run until they reach the "SAT" status, meaning "satisfied" or UNSAT. The harder the problem the longer you might be running the program - days, weeks even.

Ideally, what you want is a single SAT value among a remainder universe of UNSATs.

Sometimes the best you can achieve at any given point is a lower bound and an upper bound range, like "greater than 3 but less than 9."

Of course I simplified in my post but it started out with a pretty broad range of a lower and upper bound, then narrowed further, then narrowed further, then narrowed further, etc...until the specific final result achieved K=7=SAT while every K<7=UNSAT & every K>7=UNSAT. I think it ran for a full week alone on K between 6 and 7.

You mean SMT, right?