Yes, but you still have a regress: you have to have good reason to trust the oracle.

(E.g. Yin-Yang – A tool for stress-testing SMT solvers https://news.ycombinator.com/item?id=25123138 They found a bunch of bugs in Z3 and CVC4!)