Fix a simple bug in vmx support