Can't verify with CBMC in Ubuntu c++ programs - compiler type_traits.h template specialization with wrong number of arguments

I am trying to use the CBMC Bounded Model Checker in Ubuntu for both C and C++ programs. I have downloaded gcc (4.9 v) and g++ (4.9 v) compilers and I installed the CBMC through terminal.

---

I am able to verify C programs and no problems arise using the below procedure:

Α .c file with name file2.c:

int array[10];
int sum(){
unsigned i,sum;
sum=0;
for(i=0;i<10;i++)
sum+=array[i];
}

In terminal type:

cbmc file2.c --function sum

Output:

file file2.c: Parsing
Converting
Type-checking file2
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
Unwinding loop c::sum.0 iteration 1 file file2.c line 5 function sum thread 0
Unwinding loop c::sum.0 iteration 2 file file2.c line 5 function sum thread 0
Unwinding loop c::sum.0 iteration 3 file file2.c line 5 function sum thread 0
Unwinding loop c::sum.0 iteration 4 file file2.c line 5 function sum thread 0
Unwinding loop c::sum.0 iteration 5 file file2.c line 5 function sum thread 0
Unwinding loop c::sum.0 iteration 6 file file2.c line 5 function sum thread 0
Unwinding loop c::sum.0 iteration 7 file file2.c line 5 function sum thread 0
Unwinding loop c::sum.0 iteration 8 file file2.c line 5 function sum thread 0
Unwinding loop c::sum.0 iteration 9 file file2.c line 5 function sum thread 0
Unwinding loop c::sum.0 iteration 10 file file2.c line 5 function sum thread 0
size of program expression: 71 steps
simple slicing removed 0 assignments
Generated 0 VCC(s), 0 remaining after simplification
VERIFICATION SUCCESSFUL

---

When I try to execute the following .cpp file I get an error.

sum_num.cpp file:

// This program adds two numbers and prints their sum.
#include <iostream>

int main()
{
  int a;
  int b;
  int sum;

  sum = a + b;

  std::cout<<"The sum of "<<a<<" and "<<b<<" is "<<sum<<"\n";

  return 0;
}

Type in terminal:

cbmc sum_num.cpp --function main

Output - Error:

file sum_num.cpp: Parsing
Converting
Type-checking sum_num
file /usr/include/c++/4.9/ext/type_traits.h line 172: template specialization with wrong number of arguments
CONVERSION ERROR

Apparently, at the time being cbmc has limited support for templates and does not cover all of their potential uses.

Until the situation changes, you can either:

1. roll-back to a c++ distribution which does not have such template usage in the file /usr/include/c++/4.9/ext/type_traits.h (4.8 does have it too, so an older one)

2. remove #include<iostream> and rely on the standard C printf() function:

   #include<stdio.h>
   
   int main()
   {
       int a;
       int b;
       int sum;
   
       sum = a + b;
   
       printf("The sum of %d and %d is %d\n", a, b, sum);
   
       return 0;
   }
   

Both of these suggestions have been proposed HERE.