Exciting. And the cache size is likely the main reason.
But that can not be concluded from the analysis.
>>VTune agrees, and says that Z3 spends a lot of time waiting on memory while iterating through watched literals.
But how much is "a lot" is not specified. And the propagation also allocates memory sometimes, to keep the learned clauses. Not sure how Z3 manages this, but couldn't it be that the mallocs are just slower on that desktop, so an OS issue?
>>VTune agrees, and says that Z3 spends a lot of time waiting on memory while iterating through watched literals.
But how much is "a lot" is not specified. And the propagation also allocates memory sometimes, to keep the learned clauses. Not sure how Z3 manages this, but couldn't it be that the mallocs are just slower on that desktop, so an OS issue?