* IMachine: Add an abstract method `is_true` to evaluate an
		expression.
	* StackBasedMachine:
		* `is_true` implementation;
		* `__init__` takes a program in input;
		* `push_onto_stack`: enforce that any element in
		  memory is a `z3.BitVec` element.