I think the surprise comes from how long it takes to get the answer, not that it's incorrect.
By comparison, gcc is able to reduce those two implementations to the same thing and prove them equal in a fraction of the time (https://godbolt.org/z/6oMEd8ebY). If it takes Symbolica a minute for the same tiny example, how does it work on real codebases?
By comparison, gcc is able to reduce those two implementations to the same thing and prove them equal in a fraction of the time (https://godbolt.org/z/6oMEd8ebY). If it takes Symbolica a minute for the same tiny example, how does it work on real codebases?