diff --git a/appveyor.yml b/appveyor.yml
index 28749ffc5e6..8001e268ea1 100644
--- a/appveyor.yml
+++ b/appveyor.yml
@@ -86,19 +86,6 @@ test_script:
     rmdir /s /q cbmc\byte_update7
     rmdir /s /q cbmc\pipe1
     rmdir /s /q cbmc\unsigned___int128
-    rmdir /s /q cbmc-cpp
-    rmdir /s /q cpp\Decltype1
-    rmdir /s /q cpp\Decltype2
-    rmdir /s /q cpp\Function_Overloading1
-    rmdir /s /q cpp\Resolver10
-    rmdir /s /q cpp\Resolver11
-    rmdir /s /q cpp\Template_Parameters1
-    rmdir /s /q cpp\enum2
-    rmdir /s /q cpp\enum7
-    rmdir /s /q cpp\enum8
-    rmdir /s /q cpp\nullptr1
-    rmdir /s /q cpp\sizeof1
-    rmdir /s /q cpp\static_assert1
     rmdir /s /q goto-gcc
     rmdir /s /q goto-instrument\slice08
     cd ..
diff --git a/regression/cpp/Constant2/main.cpp b/regression/cpp/Constant2/main.cpp
index 73de7bee948..4021c39fcb6 100644
--- a/regression/cpp/Constant2/main.cpp
+++ b/regression/cpp/Constant2/main.cpp
@@ -1,10 +1,8 @@
-#include <cassert>
-
 int const C=10;
 
 int main()
 {
-  assert(C==10);
+  __CPROVER_assert(C == 10, "");
 
   // this is *not* allowed
   ((int &)C)=20;
diff --git a/regression/cpp/Function_Overloading1/main.cpp b/regression/cpp/Function_Overloading1/main.cpp
index de23c697a2c..211f1fa5554 100644
--- a/regression/cpp/Function_Overloading1/main.cpp
+++ b/regression/cpp/Function_Overloading1/main.cpp
@@ -1,17 +1,23 @@
+#ifdef __GNUC__
+#define NOTHROW __attribute__((nothrow))
+#else
+#define NOTHROW
+#endif
+
 namespace std {
   // cmath
-  __inline float abs(float x) __attribute__((nothrow));
-  __inline double abs(double x) __attribute__((nothrow));
-  __inline long double abs(long double x) __attribute__((nothrow));
+  __inline float abs(float x) NOTHROW;
+  __inline double abs(double x) NOTHROW;
+  __inline long double abs(long double x) NOTHROW;
 }
 
 namespace std {
   extern "C" {
-    int abs(int) __attribute__((nothrow)) ;
+    int abs(int) NOTHROW ;
   }
   extern "C++" {
-    inline long abs(long n) __attribute__((nothrow));
-    inline long long abs(long long n) __attribute__((nothrow));
+    inline long abs(long n) NOTHROW;
+    inline long long abs(long long n) NOTHROW;
   }
 }
 
diff --git a/regression/cpp/Resolver10/main.cpp b/regression/cpp/Resolver10/main.cpp
index 449bba39f65..9a5884f15f8 100644
--- a/regression/cpp/Resolver10/main.cpp
+++ b/regression/cpp/Resolver10/main.cpp
@@ -1,5 +1,3 @@
-#include <cassert>
-
 struct A
 {
   int i;
diff --git a/regression/cpp/Resolver11/main.cpp b/regression/cpp/Resolver11/main.cpp
index 5d503db7b0e..202ea269de5 100644
--- a/regression/cpp/Resolver11/main.cpp
+++ b/regression/cpp/Resolver11/main.cpp
@@ -1,5 +1,3 @@
-#include <cassert>
-
 struct A
 {
   bool func() { return false; }
diff --git a/regression/cpp/Template_Parameters1/main.cpp b/regression/cpp/Template_Parameters1/main.cpp
index b16c1a5eb34..cfce7164baa 100644
--- a/regression/cpp/Template_Parameters1/main.cpp
+++ b/regression/cpp/Template_Parameters1/main.cpp
@@ -1,5 +1,3 @@
-#include <cassert>
-
 // V depends on Ty
 template<typename Ty, Ty V>
 class T
diff --git a/regression/cpp/enum7/test.desc b/regression/cpp/enum7/test.desc
index a003b07b93c..5893356edf6 100644
--- a/regression/cpp/enum7/test.desc
+++ b/regression/cpp/enum7/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cpp/enum8/main.cpp b/regression/cpp/enum8/main.cpp
index b948ef723b0..bea48bf8619 100644
--- a/regression/cpp/enum8/main.cpp
+++ b/regression/cpp/enum8/main.cpp
@@ -1,5 +1,3 @@
-#include <cassert>
-
 enum E1 { e1 } e1_var;
 enum E2 { e2 } e2_var;
 
@@ -23,19 +21,19 @@ struct some_struct
 
 int main()
 {
-  assert(f(0)==0);
-  assert(f(e1)==1);
-  assert(f(e2)==2);
-  assert(f(e1_var)==1);
-  assert(f(e2_var)==2);
-
-  assert(g(0)==0);
-  assert(g(e1)==1);
-  assert(g(e2)==0);
-  assert(g(e1_var)==1);
-  assert(g(e2_var)==0);
-
-  assert(f(some_struct_var.i)==0);
-  assert(f(some_struct_var.e1)==1);
-  assert(f(some_struct_var.e2)==2);
+  __CPROVER_assert(f(0) == 0, "");
+  __CPROVER_assert(f(e1) == 1, "");
+  __CPROVER_assert(f(e2) == 2, "");
+  __CPROVER_assert(f(e1_var) == 1, "");
+  __CPROVER_assert(f(e2_var) == 2, "");
+
+  __CPROVER_assert(g(0) == 0, "");
+  __CPROVER_assert(g(e1) == 1, "");
+  __CPROVER_assert(g(e2) == 0, "");
+  __CPROVER_assert(g(e1_var) == 1, "");
+  __CPROVER_assert(g(e2_var) == 0, "");
+
+  __CPROVER_assert(f(some_struct_var.i) == 0, "");
+  __CPROVER_assert(f(some_struct_var.e1) == 1, "");
+  __CPROVER_assert(f(some_struct_var.e2) == 2, "");
 }
diff --git a/regression/cpp/nullptr1/main.cpp b/regression/cpp/nullptr1/main.cpp
index 6d178630634..5ea0c43d582 100644
--- a/regression/cpp/nullptr1/main.cpp
+++ b/regression/cpp/nullptr1/main.cpp
@@ -1,5 +1,3 @@
-#include <cassert>
-
 typedef decltype(nullptr) nullptr_t;
 
 static_assert(nullptr==0, "nullptr==0");
@@ -20,7 +18,7 @@ int main()
 
   char buffer[10];
   void *p=my_null, *q=buffer;
-  assert(q!=nullptr);
+  __CPROVER_assert(q != nullptr, "");
 
   something(nullptr);
 }
diff --git a/src/goto-cc/ms_cl_cmdline.cpp b/src/goto-cc/ms_cl_cmdline.cpp
index 7364beca6ba..58a0736ed06 100644
--- a/src/goto-cc/ms_cl_cmdline.cpp
+++ b/src/goto-cc/ms_cl_cmdline.cpp
@@ -406,6 +406,7 @@ const char *ms_cl_prefixes[]=
   "MT", //  link with LIBCMT.LIB
   "MDd", //  link with MSVCRTD.LIB debug lib
   "MTd", //  link with LIBCMTD.LIB debug lib
+  "std", //  specify C++ language standard
   nullptr
 };
 
diff --git a/src/goto-cc/ms_cl_mode.cpp b/src/goto-cc/ms_cl_mode.cpp
index 4e9c3789c19..5a459ac048c 100644
--- a/src/goto-cc/ms_cl_mode.cpp
+++ b/src/goto-cc/ms_cl_mode.cpp
@@ -77,6 +77,30 @@ int ms_cl_modet::doit()
   else
     compiler.mode=compilet::COMPILE_LINK_EXECUTABLE;
 
+  if(cmdline.isset("std"))
+  {
+    const std::string std_string = cmdline.get_value("std");
+
+    if(
+      std_string == ":c++14" || std_string == "=c++14" ||
+      std_string == ":c++17" || std_string == "=c++17" ||
+      std_string == ":c++latest" || std_string == "=c++latest")
+    {
+      // we don't have any newer version at the moment
+      config.cpp.set_cpp14();
+    }
+    else if(std_string == ":c++11" || std_string == "=c++11")
+    {
+      // this isn't really a Visual Studio variant, we just do this for GCC
+      // command-line compatibility
+      config.cpp.set_cpp11();
+    }
+    else
+      warning() << "unknown language standard " << std_string << eom;
+  }
+  else
+    config.cpp.set_cpp14();
+
   compiler.echo_file_name=true;
 
   if(cmdline.isset("Fo"))