Freshness manager synchronization

[berpeti]

The current version of the freshness manager is not synchronized. The user of the library can create fresh variables manually, leading to an inconsistent state in the freshness manager. To tackle this issue, all freshness manager tactics could do a synchronization first (by putting all variables that are not inside the manager into the list of variables that should be avoided).

[h0nzZik]

I am not sure if this is possible. The manager also maintains a list of variables that are distinct from the ones in the avoid list. What if the user creates a variable which would not be fresh enough to be added to the avoid list? Also, what is the use case for this?