Repository to recreate the reported issue on WPI non terminating.
Configure the CF_BINARY in run_wpi.py and /wpi/wpi.sh
cd wpi
python3 run_wpi.py
After execution, the resulting .ajava files will be stored for each benchmark in the directory root-dir/dataset/benchmark-directory/src/wpi-iterations.
The results of running the checker before and after WPI inference can be found in root-dir/wpi/checkerframework-3.34.0-results-WPI.
In the dataset folder:
SimplifiedTestCodecontains the simplified test case.url49526af437_Maria_G_CS325_tgz-pJ8-assignments_farmer_FarmerImplJ8is the complete sample benchmark for which we encountered the non-termination issue.MoreSamplesOfChallengingBenchmarkscontains more benchmarks with the same issue.