Test file does not run properly after #566

[bclement-ocp]

I think this is an issue of old tests/issues/dune being re-used by the CI?

Locally it is fixed by cleaning this file

@Halbaroth

[bclement-ocp]

Actually: looks like tests for issue #505 almost timeout with the timelimit of 2 (I get around 1.9s on my machine which is presumaby more powerful than gh CI).

Maybe we should drop them?

[bclement-ocp]

Although this looks like a perf regression compared to 2.4.3 where I get about .5s :cry:

[bclement-ocp]

The slowdown seems to be limited to use of the --no-minimal-bj option

[bclement-ocp]

Bisecting points to 7d691157db940d7853e1f1d235031589d26372fa as the commit where --no-minimal-bj gets slower, but unfortunately this seems to be a weak-table-bug: I get about a 5% increase in the numbers of steps to resolution when adding that commit, but no change when running with --disable-weak.

I would suggest to either disable these tests for now, or increase the tests timeout to 3s. @Halbaroth what do you think?

[Halbaroth]

I think we can keep too long non-regression tests on Marvin. We should keep them to be sure our modifications will not reopen an old issue.

[bclement-ocp]

I am fine with that. Do we have a process for marking these tests as "too long non-regression tests"? Should they be moved from the tests directory to elsewhere?

[Halbaroth]

I think we should create one directory by test sets and we can create a issue test sets for instance. Basically,

• tests/
• tests/smtlib
• tests/internals
• tests/issues

[bclement-ocp]

Not sure how that solves the issue, I believe make runtest (and make runtest-ci) run everything in the tests directory?

[Halbaroth]

Sorry, it was misleading. I was talking about the tests directory on Marvin. We will remove the failed test from the tests directory on GitHub.

[bclement-ocp]

Ah, OK. But we should probably keep these tests in the repo as well, it's a fluke that they are slow currently

I'll place them in a slow_tests directory for now