Fix example proof scripts that were broken by function renames (#955).

[brianhuffman]

This should make the test_examples integration test work again.

See also #995.

[RyanGlScott]

Does this fix #994? Also, does this mean that we can remove test_examples from the list of broken tests in the following places?

• saw-script/.travis.yml

  Line 67 in 9a9274c

  - for t in test0001 test0019_jss_switch_statement test_crucible_jvm test_ecdsa test_examples test_issue108 test_tutorial1 test_tutorial2 test_tutorial_w4; do echo $t >> disabled_tests.txt; done

• saw-script/.github/ci.sh

  Line 173 in 8ad4bf5

  for t in test0001 test0019_jss_switch_statement test_crucible_jvm test_ecdsa test_examples test_issue108 test_tutorial1 test_tutorial2 test_tutorial_w4; do echo $t >> disabled_tests.txt; done

[brianhuffman]

I believe the specific problems mentioned in #994 (related to java extraction) were actually fixed by #988 (commits 90a2842 and 42628aa). This PR fixes a couple of other examples that were not java-related, but became broken at the same time, due to botched function renamings in #980.

And, yes, I suppose this means that we could re-enable test_examples in those CI scripts, although I don't know the reason why they were excluded in the first place. If it was due to resource limits, that may still be a problem, as test_examples does take a non-trivial amount of time to run.

[brianhuffman]

Another question: Is that really a "list of broken tests"? I imagine that different tests might be excluded for different reasons: They could be broken, only work on a specific OS, take too long to run, or maybe require certain solvers that are/were not available in the CI environment. It would be nice to add comments indicating why each one is excluded; that would make it easier for someone else to decide if/when it's appropriate to add them back in.

If any of them are actually broken, we should really have open tickets for each such broken test.

[RyanGlScott]

Unfortunately, I don't have much insight as to why these tests were excluded in the first place. I agree that we should do a better job of tracking why things are not run on CI—perhaps #995 can become the central tracking issue for that?

As far as whether test_examples takes too long to run on CI... there's only one way to find out, right? I say we re-enable it and see what happens :)

[brianhuffman]

So it sounds like you're suggesting I re-enable test_examples in ci.sh as part of this PR, and see if it works? Ok, I'll give it a go.

[brianhuffman]

It looks like the integration tests are working just fine with test_examples included. However it looks like the run-time has increased significantly: The "details" link indicates that the integration tests took about 9 minutes to run, while on other recent PRs (with test_examples excluded) the integration tests have been finishing in less than 5 minutes.

It's probably worth increasing the CI time to get better test coverage. If the CI run-time is (or becomes) a problem, we should probably focus on tweaking the test proof scripts to run faster instead of disabling the tests.

[RyanGlScott]

It's probably worth increasing the CI time to get better test coverage. If the CI run-time is (or becomes) a problem, we should probably focus on tweaking the test proof scripts to run faster instead of disabling the tests.

I certainly wouldn't object to making things run faster. Alternatively, if certain tests are just too long-running to have run on every single PR, we could also consider only running them in the nightly configuration.

[robdockins]

I think keeping the examples unbroken is worth the CI time, but maybe @RyanGlScott's idea to push some things into a nightly configuration is also worthwhile.