WBS 3 steps in TCG JR Mode shows more tests than possible obligations

vaibhavbsharma / java-ranger

Java Ranger is a path-merging extension of Symbolic PathFinder

https://github.com/SymbolicPathFinder/jpf-symbc

13 stars 5 forks source link

WBS 3 steps in TCG JR Mode shows more tests than possible obligations #9

Open sohah opened 4 years ago

sohah commented 4 years ago

Something is going wrong with WBS in JR mode when running it with 3 steps. This is happening for both the guiding and the collect modes. Basically more test cases are generated than possible since they are more than the total number of obligations in WBS.