Cannot fix a bug with a test suite, but fix it correctly with a subset of the test suite

Question

Cannot fix a bug with a test suite, but fix it correctly with a subset of the test suite

Amirfarhad-Nilizadeh opened this issue 4 years ago · 4 comments

Amirfarhad-Nilizadeh commented 4 years ago

A buggy program in a BuggyJava+JML dataset can be fixed correctly with a test suite using Nopol in less than 10 seconds. However, when I add some more tests to the test suite, then after around 8 minutes, it cannot fix it (generates a "solver.out.z3" file, but not a patch).

What can be the reason?

Is there any time limitation for running to validate a candidate patch in Nopol? Maybe this time is not enough to run the larger test suite. If any limitation exists to validate a candidate patch, does any option consider managing that time to execute a candidate patch?

Answer 1 · 2021-02-05T11:01:55.000Z

More tests means that the generated SMT problem is larger. You can see that by intercepting the SmtLib commands. I don't recall the complexity of the generated SMT problem, but I would not be surprised if it is superlinear wrt the number of tests.

Answer 2 · 2021-02-05T21:31:46.000Z

Thank you so much.

It makes sense; also, giving more time to the Nopol (SMT Solver) cannot solve this problem. Please let me know if this is not correct.

One more question related to this observation. Is Nopol's output deterministic with a test suite? I run it several times, and each time its output was the same.

Answer 3 · 2021-02-08T12:51:39.000Z

in theory, yes, only if if the underlying program is deterministic.

Answer 4 · 2021-02-09T02:11:58.000Z

Thank you for your quick response.