3 ms·
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.ycombi
by carapace 6y ago
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 https://news.ycombinator.com/item?id=25123138 They found a bunch of bugs in Z3 and CVC4!)