Bug in SMT.getModel(), after too many push/pop operations a valid query reports an error referring to a variable '@4'