DEBUG

Author: tautschnig

regression/cbmc/cprover_bool1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---trace
+--trace --preprocess
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

src/goto-symex/goto_state.cpp

@@ -12,6 +12,8 @@ Author: Romain Brenguier, [email protected]
 
 #include <util/format_expr.h>
 
+#include <iostream>
+
 /// Print the constant propagation map in a human-friendly format.
 /// This is primarily for use from the debugger; please don't delete me just
 /// because there aren't any current callers.
@@ -146,6 +148,9 @@ void goto_statet::apply_condition(
     else if(rhs.is_false())
       apply_condition(equal_exprt{lhs, true_exprt{}}, previous_state, ns);
     else
+    {
+      std::cerr << condition.pretty() << std::endl;
       UNREACHABLE;
+    }
   }
 }