diff --git a/regression/cbmc-concurrency/memory_barrier2/msvc.desc b/regression/cbmc-concurrency/memory_barrier2/msvc.desc
index 9327f8de9a5..91f366f8aeb 100644
--- a/regression/cbmc-concurrency/memory_barrier2/msvc.desc
+++ b/regression/cbmc-concurrency/memory_barrier2/msvc.desc
@@ -1,5 +1,5 @@
 CORE
-msvc.c
+msvc.i
 --mm tso --winx64
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/cbmc-concurrency/memory_barrier2/msvc.c b/regression/cbmc-concurrency/memory_barrier2/msvc.i
similarity index 83%
rename from regression/cbmc-concurrency/memory_barrier2/msvc.c
rename to regression/cbmc-concurrency/memory_barrier2/msvc.i
index b36e9a1be00..89ef92d50ed 100644
--- a/regression/cbmc-concurrency/memory_barrier2/msvc.c
+++ b/regression/cbmc-concurrency/memory_barrier2/msvc.i
@@ -1,3 +1,8 @@
+void __asm_mfence(void)
+{
+  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
+}
+
 volatile int turn;
 int x;
 volatile int flag1 = 0, flag2 = 0;
diff --git a/regression/cbmc-library/__asm_fstcw-01/msvc.desc b/regression/cbmc-library/__asm_fstcw-01/msvc.desc
index 0275139a2df..780e6502916 100644
--- a/regression/cbmc-library/__asm_fstcw-01/msvc.desc
+++ b/regression/cbmc-library/__asm_fstcw-01/msvc.desc
@@ -1,5 +1,5 @@
 CORE
-msvc.c
+msvc.i
 --pointer-check --bounds-check --winx64
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/cbmc-library/__asm_fstcw-01/msvc.c b/regression/cbmc-library/__asm_fstcw-01/msvc.i
similarity index 66%
rename from regression/cbmc-library/__asm_fstcw-01/msvc.c
rename to regression/cbmc-library/__asm_fstcw-01/msvc.i
index 11c1cf19932..e9de7276048 100644
--- a/regression/cbmc-library/__asm_fstcw-01/msvc.c
+++ b/regression/cbmc-library/__asm_fstcw-01/msvc.i
@@ -1,3 +1,10 @@
+extern int __CPROVER_rounding_mode;
+
+void __asm_fstcw(void *dest)
+{
+  *(unsigned short *)dest = __CPROVER_rounding_mode << 10;
+}
+
 int main()
 {
   unsigned short cw;