title: Can't verify with CBMC in Ubuntu c++ programs - compiler type_traits.h template specialization with wrong number of arguments
body: <p>I am trying to use the <a href="http://www.cprover.org/cbmc/" rel="nofollow">CBMC</a> 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.</p>
  
  <hr>
  
  <p>I am able to verify C programs and no problems arise using the below procedure:</p>
  
  <p>Α .c file with name <code>file2.c</code>:</p>
  
  <pre><code>int array[10];
  int sum(){
  unsigned i,sum;
  sum=0;
  for(i=0;i&lt;10;i++)
  sum+=array[i];
  }
  </code></pre>
  
  <p>In terminal type:</p>
  
  <pre><code>cbmc file2.c --function sum
  </code></pre>
  
  <p>Output:</p>
  
  <pre><code>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
  </code></pre>
  
  <hr>
  
  <p>When I try to execute the following .cpp file I get an error.</p>
  
  <p><code>sum_num.cpp</code> file:</p>
  
  <pre><code>// This program adds two numbers and prints their sum.
  #include &lt;iostream&gt;
  
  int main()
  {
    int a;
    int b;
    int sum;
  
    sum = a + b;
  
    std::cout&lt;&lt;"The sum of "&lt;&lt;a&lt;&lt;" and "&lt;&lt;b&lt;&lt;" is "&lt;&lt;sum&lt;&lt;"\n";
  
    return 0;
  }
  </code></pre>
  
  <p>Type in terminal:</p>
  
  <pre><code>cbmc sum_num.cpp --function main
  </code></pre>
  
  <p>Output - Error:</p>
  
  <pre><code>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
  </code></pre>