Conversation
39cfbce to
e211c28
Compare
Randomized DFS shuffles the queue of successor states
e211c28 to
cec0d94
Compare
|
I assume symex is dead since these PRs have sat here for 2 years without anyone noticing and the master branch fails all CI? If that's the case I won't bother rebasing |
|
I think symex may be dead. Most of the symex-like functionality is now in CBMC which (thanks to @karkhaz @tautschnig @peterschrammel ) can do per-path analysis. |
|
RIP symex. I won't re-implement these PRs for the per-path analysis though, since I was the sole user and I'm no longer using it. The ideas behind them weren't that novel, so the only thing lost if these die is coding effort. |
|
However, the depth-first search mode in CBMC isn't randomized, it's just a standard DFS. Implementing a randomized version shouldn't be very difficult, though. Happy to help if anyone still needs this feature. |
|
Whoops, sorry Khareem, posted at the same time. |
Introduce randomized DFS search.
I have used the command line option --randomized in combination with --dfs, because in a future pull request I also use this to randomize a shortest path based search heuristic