[code refactoring] create an interface for variables to values map
A map from variables in scope to values is the core element of a counterexample step, a test step, or the unsatisfiability witness returned by Z3.
Create an interface for this kind of map, which will be used by multiple formal checks. Additionally, refactor the code converting a counterexample to a simulation trace using this interface.
(from redmine: issue id 3619, created on 2019-01-20)