diff --git a/devicemodel/core/main.c b/devicemodel/core/main.c index bd65beaac..41bd11710 100644 --- a/devicemodel/core/main.c +++ b/devicemodel/core/main.c @@ -907,6 +907,8 @@ main(int argc, char *argv[]) break; case CMD_OPT_LAPIC_PT: lapic_pt = true; + is_rtvm = true; + break; case CMD_OPT_RTVM: is_rtvm = true; break;