Print status information upon reaching assume(false)

Author: tautschnig

src/cbmc/symex_bmc.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include <limits>
 
 #include <util/source_location.h>
+#include <util/simplify_expr.h>
 
 #include "symex_bmc.h"
 
@@ -67,6 +68,21 @@ void symex_bmct::symex_step(
      !state.guard.is_false())
     symex_coverage.covered(state.source.pc);
 
+  if(!state.guard.is_false() &&
+     state.source.pc->is_assume() &&
+     simplify_expr(state.source.pc->guard, ns).is_false())
+  {
+    statistics() << "aborting path on assume(false) at "
+                 << state.source.pc->source_location
+                 << " thread " << state.source.thread_nr;
+
+    const irep_idt &c=state.source.pc->source_location.get_comment();
+    if(!c.empty())
+      statistics() << ": " << c;
+
+    statistics() << eom;
+  }
+
   goto_symext::symex_step(goto_functions, state);
 }
 

src/symex/path_search.cpp

@@ -6,6 +6,7 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#include <util/simplify_expr.h>
 #include <util/time_stopping.h>
 
 #include <solvers/flattening/bv_pointers.h>
@@ -315,8 +316,10 @@ Function: path_searcht::drop_state
 
 \*******************************************************************/
 
-bool path_searcht::drop_state(const statet &state) const
+bool path_searcht::drop_state(const statet &state)
 {
+  goto_programt::const_targett pc=state.get_instruction();
+
   // depth limit
   if(depth_limit_set && state.get_depth()>depth_limit)
     return true;
@@ -345,6 +348,22 @@ bool path_searcht::drop_state(const statet &state) const
         return true;
   }
 
+  if(pc->is_assume() &&
+     simplify_expr(pc->guard, ns).is_false())
+  {
+    debug() << "aborting path on assume(false) at "
+            << pc->source_location
+            << " thread " << state.get_current_thread();
+
+    const irep_idt &c=pc->source_location.get_comment();
+    if(!c.empty())
+      debug() << ": " << c;
+
+    debug() << eom;
+
+    return true;
+  }
+
   return false;
 }
 

src/symex/path_search.h

@@ -120,7 +120,7 @@ class path_searcht:public safety_checkert
   bool is_feasible(statet &state);
   void do_show_vcc(statet &state);
 
-  bool drop_state(const statet &state) const;
+  bool drop_state(const statet &state);
 
   void report_statistics();