Closed oflatt closed 1 year ago
This PR simplifies rational_best, which makes herbie perform better The branch is called "unsound" because the z3 verifier still allows dropping variables (which is unsound)
Thanks for the review, fixed it up @ajpal
Spoke too soon, need to fix up a test
This PR simplifies rational_best, which makes herbie perform better The branch is called "unsound" because the z3 verifier still allows dropping variables (which is unsound)