diff --git a/appveyor.yml b/appveyor.yml
index 7fe07b6da72..c61f77b99b4 100644
--- a/appveyor.yml
+++ b/appveyor.yml
@@ -83,6 +83,7 @@ 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
diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt
index 58558146ecd..b710bf9df0a 100644
--- a/regression/CMakeLists.txt
+++ b/regression/CMakeLists.txt
@@ -25,10 +25,13 @@ endmacro(add_test_pl_tests)
 
 add_subdirectory(ansi-c)
 add_subdirectory(cbmc)
+add_subdirectory(cbmc-cover)
+add_subdirectory(cbmc-cpp)
 add_subdirectory(cbmc-java)
 add_subdirectory(cbmc-java-inheritance)
 add_subdirectory(cpp)
 add_subdirectory(goto-analyzer)
+add_subdirectory(goto-analyzer-taint)
 add_subdirectory(goto-cc-cbmc)
 add_subdirectory(goto-cc-goto-analyzer)
 add_subdirectory(goto-diff)
diff --git a/regression/Makefile b/regression/Makefile
index 418a2501dde..ef66ce3b2a0 100644
--- a/regression/Makefile
+++ b/regression/Makefile
@@ -1,6 +1,7 @@
 DIRS = ansi-c \
        cbmc \
        cbmc-cover \
+       cbmc-cpp \
        cbmc-java \
        cbmc-java-inheritance \
        cpp \
diff --git a/regression/cbmc-cover/CMakeLists.txt b/regression/cbmc-cover/CMakeLists.txt
new file mode 100644
index 00000000000..93d5ee716c2
--- /dev/null
+++ b/regression/cbmc-cover/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc>"
+)
diff --git a/regression/cbmc-cpp/CMakeLists.txt b/regression/cbmc-cpp/CMakeLists.txt
new file mode 100644
index 00000000000..93d5ee716c2
--- /dev/null
+++ b/regression/cbmc-cpp/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc>"
+)
diff --git a/regression/cbmc-cpp/FunctionParam1/main.cpp b/regression/cbmc-cpp/FunctionParam1/main.cpp
new file mode 100644
index 00000000000..3ed989a7073
--- /dev/null
+++ b/regression/cbmc-cpp/FunctionParam1/main.cpp
@@ -0,0 +1,12 @@
+#include <assert.h>
+int x;
+
+void g(int i){
+  x=i;
+}
+
+int main() {
+  g(3);
+  assert(x==3);
+}
+
diff --git a/regression/cbmc-cpp/FunctionParam1/test.desc b/regression/cbmc-cpp/FunctionParam1/test.desc
new file mode 100644
index 00000000000..91d9cf8b52e
--- /dev/null
+++ b/regression/cbmc-cpp/FunctionParam1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-cpp/MethodParam1/main.cpp b/regression/cbmc-cpp/MethodParam1/main.cpp
new file mode 100644
index 00000000000..78240ce8bd2
--- /dev/null
+++ b/regression/cbmc-cpp/MethodParam1/main.cpp
@@ -0,0 +1,18 @@
+#include <assert.h>
+unsigned x;
+
+class ct {
+  void f(int i) {
+    x=x+i;
+  }
+};
+
+int main() {
+  unsigned r;
+  x=r%3;
+  ct c;
+  c.f(2);
+  assert(x<4);
+  assert(x<5);
+}
+
diff --git a/regression/cbmc-cpp/MethodParam1/test.desc b/regression/cbmc-cpp/MethodParam1/test.desc
new file mode 100644
index 00000000000..2e6283f7316
--- /dev/null
+++ b/regression/cbmc-cpp/MethodParam1/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.cpp
+
+instance is SATISFIABLE$
+instance is UNSATISFIABLE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc-cpp/union2/main.cpp b/regression/cbmc-cpp/union2/main.cpp
index 3981fff6d46..4fbcc4e0de5 100644
--- a/regression/cbmc-cpp/union2/main.cpp
+++ b/regression/cbmc-cpp/union2/main.cpp
@@ -1,3 +1,4 @@
+#include <assert.h>
 struct A
 {
   union
diff --git a/regression/goto-analyzer-taint/CMakeLists.txt b/regression/goto-analyzer-taint/CMakeLists.txt
new file mode 100644
index 00000000000..73af8689568
--- /dev/null
+++ b/regression/goto-analyzer-taint/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:goto-analyzer>"
+)
diff --git a/src/cpp/cpp_typecheck_function.cpp b/src/cpp/cpp_typecheck_function.cpp
index 06739870df6..8081368e290 100644
--- a/src/cpp/cpp_typecheck_function.cpp
+++ b/src/cpp/cpp_typecheck_function.cpp
@@ -44,8 +44,9 @@ void cpp_typecheckt::convert_parameter(
   symbol.type=parameter.type();
   symbol.is_state_var=true;
   symbol.is_lvalue=!is_reference(symbol.type);
+  symbol.is_parameter=true;
 
-  assert(!symbol.base_name.empty());
+  INVARIANT(!symbol.base_name.empty(), "parameter has base name");
 
   symbolt *new_symbol;