Fix has_done_something and fixpoint logic
#545
Merged
has_done_something and fixpoint logic
#545