Fixed slicing of nodes with multiple outputs
Fixed substitution of variables by definitions in quantifier elimination