Debugging

Author: tautschnig

regression/cbmc/SIMD1/program.desc

@@ -0,0 +1,8 @@
+CORE broken-smt-backend
+main.c
+--show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/SIMD1/test.desc

@@ -1,6 +1,6 @@
 CORE broken-smt-backend
 main.c
---stop-on-fail
+--trace
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

src/solvers/flattening/bv_utils.cpp

@@ -8,6 +8,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "bv_utils.h"
 
+#include <iostream>
+
 bvt bv_utilst::build_constant(const mp_integer &n, std::size_t width)
 {
   std::string n_str=integer2binary(n, width);
@@ -382,6 +384,8 @@ bvt bv_utilst::saturating_add_sub(
   result.reserve(add_sub_result.size());
   if(rep == representationt::UNSIGNED)
   {
+    std::cerr << "Unsigned saturating arithmetic over " << add_sub_result.size()
+      << " bits with subtract=" << subtract << std::endl;
     // An unsigned overflow has occurred when carry_out is not equal to
     // subtract: addition with a carry-out means an overflow beyond the maximum
     // representable value, subtraction without a carry-out means an underflow
@@ -396,6 +400,8 @@ bvt bv_utilst::saturating_add_sub(
   }
   else
   {
+    std::cerr << "Signed saturating arithmetic over " << add_sub_result.size()
+      << " bits with subtract=" << subtract << std::endl;
     // A signed overflow beyond the maximum representable value occurs when
     // adding two positive numbers and the wrap-around result being negative, or
     // when subtracting a negative from a positive number (and, again, the