Open gernst opened 2 years ago
Observation about scoring: If we find small win/try using random sampling that is actually an indication that we should symbolically check if there is a rare branch, and that is the opposite of the current score.
Perhaps look at #phantom nodes in a subtree to guide the search?
The current implementation computes one sample using Z3 for each binary execution. We should probably run many executions per such sample, where the input prefix just stays the same, whereas the rest of the inputs varies randomly.
Technically, we should refactor the main loop using some extra functions, such that the control flow works out fine.