Inconsistent variable state after solveAll #788
Description
There is an inconsistency between the solvers based on what the values of the variables should be after a .solveAll() call and all solutions have been enumerated. Solvers with native solveAll support often still hold the last found solution as the variables' .value(). But Z3, which depends on the solveAll in the abstract SolverInterface, makes use of blocking constraints (nogoods) to force a different solution for each .solve() call. When all solutions have been enumerated, .solve() returns unsat and the variables all have 'None' values. This difference makes tests related to #780 fail.
To make the behavior consistent, we would have to keep track of the last solution found by SolverInterface.solveAll() and upon unsat restore this solution. Other option is to make all other solvers clean/reset their solution. The former seems the most consistent behavior across solvers and require the least change.