cleaned up timer infrastructure

[palacios.git] / palacios / src / palacios / vmx.c

diff --git a/palacios/src/palacios/vmx.c b/palacios/src/palacios/vmx.c
index 3334d2f..d2e3a79 100644 (file)
--- a/palacios/src/palacios/vmx.c
+++ b/palacios/src/palacios/vmx.c
@@ -660,7 +660,7 @@ int v3_vmx_enter(struct guest_info * info) {
 
     // We do timer injection here to track real host time.
     rdtscll(tmp_tsc);
-    v3_update_time(info, tmp_tsc - info->time_state.cached_host_tsc - info->time_state.cached_hlt_tsc);
+    v3_update_time(info, tmp_tsc - info->time_state.cached_host_tsc);
     info->time_state.cached_hlt_tsc = 0;
     rdtscll(info->time_state.cached_host_tsc);