I have changed my mind and think we should have SMTContext mandatory and not an optional, as the current design makes it way too easy to give a default Nothing value when extending the code-base in the future. This then has the potential to re-introduce a similar bug. Another advantage tot his approach is the removal of the ugly pattern matching present each time we actually want to use the solver.
Instead, in this PR, the Maybe is pushed into SMTContext, where the dummy/empty instance now has to be consciously built using the new noSolver function.
The fallout is fairly minimal and we confide the logic of not having a solver to the SMT interface. I.e. the only places where not having a solver has a different behavior are:
hardReset - becomes a no-op when no solver handle is present
runCmd -> always returns the Unknown response when no solver exists
This eliminates duplicate instances of handling an unknown response vs not having a solver, since in all instances of the current code-base, they are functionally the same.
I have changed my mind and think we should have
SMTContextmandatory and not an optional, as the current design makes it way too easy to give a defaultNothingvalue when extending the code-base in the future. This then has the potential to re-introduce a similar bug. Another advantage tot his approach is the removal of the ugly pattern matching present each time we actually want to use the solver. Instead, in this PR, theMaybeis pushed intoSMTContext, where the dummy/empty instance now has to be consciously built using the newnoSolverfunction. The fallout is fairly minimal and we confide the logic of not having a solver to the SMT interface. I.e. the only places where not having a solver has a different behavior are:hardReset- becomes a no-op when no solver handle is presentrunCmd-> always returns theUnknownresponse when no solver exists This eliminates duplicate instances of handling an unknown response vs not having a solver, since in all instances of the current code-base, they are functionally the same.