This PR contains two tests: the first has a proof that can be automatically minimized, the second one cannot. I designed them to be as similar to each other as possible. This aims to isolate the issue that causes #165 and therefore provide a (hopefully) sound explanation of the phenomenon.
Additional evidence is provided by the fact that my edited version of the minimizer can find the test shortening of th2 in min_not_found.mm, which the regular minimizer cannot detect.
The following comments [1][2] have been very helpful to figure out the issue, and the test cases presented in this PR have been inspired by them.
fixes #165
This PR contains two tests: the first has a proof that can be automatically minimized, the second one cannot. I designed them to be as similar to each other as possible. This aims to isolate the issue that causes #165 and therefore provide a (hopefully) sound explanation of the phenomenon.
Additional evidence is provided by the fact that my edited version of the minimizer can find the test shortening of
th2inmin_not_found.mm, which the regular minimizer cannot detect.The following comments [1] [2] have been very helpful to figure out the issue, and the test cases presented in this PR have been inspired by them.