CPAchecker exports the tests in the reverse order
CPAchecker exports the tests in the reverse order.
Steps to reproduce:
scripts/cpa.sh -svcomp20 -heap 10000M -benchmark -timelimit '900 s' -stats -spec sv-benchmarks/properties/unreach-call.prp sv-benchmarks/c/array-tiling/skippedu.c
and then run cpa.sh -witness2test
scripts/cpa.sh -witness2test -setprop counterexample.export.exportTestCase=true -setprop testcase.xml=test.xml -setprop witness.checkProgramHash=false -witness ./output/witness.graphml -timelimit 900s -stats -spec sv-benchmarks/properties/unreach-call.prp sv-benchmarks/c/array-tiling/skippedu.c
Check Counterexample.1.harness.c
and test.xml
Expected: the test values should be in same order in both the files
Actual: test values are in reverse order. Counterexample.1.harness.c
seems to be correct.
Edited by Sudeep Kanav