@salmans you wanted me to write this down in the meeting
i believe you mean that the SMT solver, when generating a model, deals with equality, and will collapse two names into the same element. the optimization is that, the SMT solver currently keeps these collapses when asking for the next model; any equality decisions made should be thrown out when generating the next model.
if i am incorrect / not being precise enough, feel free to add / edit this issue.
@salmans you wanted me to write this down in the meeting
i believe you mean that the SMT solver, when generating a model, deals with equality, and will collapse two names into the same element. the optimization is that, the SMT solver currently keeps these collapses when asking for the next model; any equality decisions made should be thrown out when generating the next model.
if i am incorrect / not being precise enough, feel free to add / edit this issue.