On this branch: https://github.com/LAJW/cbmc/tree/lajw%2Falways-load-cprover-nondet-initialize
The following test:
jbmc/regression/jbmc/cprover-always-load-nondet-initialize/test.desc
Fails on CI and OSX. Renaming that test to test-2.desc makes it run on OSX and CI... once. On top of that, after renaming, it seems to be run twice, and the second run fails.
Removing regex entries (^EXIT=0$, ^SIGNAL=0$) is the only way to make the test pass (even though the text these regexes are looking for appears in the output).
This issue happens on Travis, Appveyor and OSX, and occasionally on Ubuntu 16.04.
On this branch: https://github.com/LAJW/cbmc/tree/lajw%2Falways-load-cprover-nondet-initialize
The following test:
Fails on CI and OSX. Renaming that test to
test-2.descmakes it run on OSX and CI... once. On top of that, after renaming, it seems to be run twice, and the second run fails.Removing regex entries (
^EXIT=0$,^SIGNAL=0$) is the only way to make the test pass (even though the text these regexes are looking for appears in the output).This issue happens on Travis, Appveyor and OSX, and occasionally on Ubuntu 16.04.