[TestComp-2022] Status `done` with the minimum test case generated

[DonggeLiu]

Issue

Legion-SymCC terminated with status done because it over-simplifies the tree.

Sample output from Legion-SymCC

tests/pals_STARTPALS_Triplicated.2.ufo.BOUNDED-10.pals/metadata.xml

?                                  input: 
return code:  -9
deterministic
done

final tree
      local      subtree
   win  try     win  try    path
*    0    0       0    0    

Command

./legion.sh -L ubuntu2004/lib -m 10000 -32 ../../sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated.2.ufo.BOUNDED-10.pals.c

Corresponding programs

seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.BOUNDED-10.pals.yml seq-mthreaded/pals_STARTPALS_Triplicated.2.ufo.BOUNDED-10.pals.yml seq-mthreaded/pals_STARTPALS_Triplicated.ufo.BOUNDED-10.pals.yml

[gernst]

The issue is that we run into e.g. segfaults (SIGBUS) where we do have alternatives (better random samples) but which do not show up symbolically.

[DonggeLiu]

In some cases, they also mentioned that the partial trace was unsupported. For example:

?                                  input: 
return code:  -9
partial trace:  unsupported
deterministic
done

final tree
      local      subtree
   win  try     win  try    path
*    0    0       0    0    

Command

./legion.sh -L ubuntu2004/lib -m 10000 -32 ../../sv-benchmarks/c/floats-cbmc-regression/float-rounding1.i

Sample program

floats-cbmc-regression/float-rounding1.yml