Print (at debug level) the current SSA step being converted

Author: tautschnig

src/goto-symex/symex_target_equation.cpp

@@ -400,10 +400,23 @@ void symex_target_equationt::convert(
 void symex_target_equationt::convert_assignments(
   decision_proceduret &decision_procedure) const
 {
+  const unsigned verbosity =
+    decision_procedure.get_message_handler().get_verbosity();
+  const bool debug_output = verbosity >= messaget::M_DEBUG;
+
   for(const auto &step : SSA_steps)
   {
     if(step.is_assignment() && !step.ignore)
+    {
+      if(debug_output)
+      {
+        std::ostringstream oss;
+        step.output(oss);
+        decision_procedure.debug() << oss.str() << messaget::eom;
+      }
+
       decision_procedure.set_to_true(step.cond_expr);
+    }
   }
 }
 
@@ -437,12 +450,22 @@ void symex_target_equationt::convert_decls(
 void symex_target_equationt::convert_guards(
   prop_convt &prop_conv)
 {
+  const unsigned verbosity = prop_conv.get_message_handler().get_verbosity();
+  const bool debug_output = verbosity >= messaget::M_DEBUG;
+
   for(auto &step : SSA_steps)
   {
     if(step.ignore)
       step.guard_literal=const_literal(false);
     else
     {
+      if(debug_output)
+      {
+        std::ostringstream oss;
+        step.output(oss);
+        prop_conv.debug() << oss.str() << messaget::eom;
+      }
+
       try
       {
         step.guard_literal = prop_conv.convert(step.guard);
@@ -462,6 +485,9 @@ void symex_target_equationt::convert_guards(
 void symex_target_equationt::convert_assumptions(
   prop_convt &prop_conv)
 {
+  const unsigned verbosity = prop_conv.get_message_handler().get_verbosity();
+  const bool debug_output = verbosity >= messaget::M_DEBUG;
+
   for(auto &step : SSA_steps)
   {
     if(step.is_assume())
@@ -470,6 +496,13 @@ void symex_target_equationt::convert_assumptions(
         step.cond_literal=const_literal(true);
       else
       {
+        if(debug_output)
+        {
+          std::ostringstream oss;
+          step.output(oss);
+          prop_conv.debug() << oss.str() << messaget::eom;
+        }
+
         try
         {
           step.cond_literal = prop_conv.convert(step.cond_expr);
@@ -490,6 +523,9 @@ void symex_target_equationt::convert_assumptions(
 void symex_target_equationt::convert_goto_instructions(
   prop_convt &prop_conv)
 {
+  const unsigned verbosity = prop_conv.get_message_handler().get_verbosity();
+  const bool debug_output = verbosity >= messaget::M_DEBUG;
+
   for(auto &step : SSA_steps)
   {
     if(step.is_goto())
@@ -498,6 +534,13 @@ void symex_target_equationt::convert_goto_instructions(
         step.cond_literal=const_literal(true);
       else
       {
+        if(debug_output)
+        {
+          std::ostringstream oss;
+          step.output(oss);
+          prop_conv.debug() << oss.str() << messaget::eom;
+        }
+
         try
         {
           step.cond_literal = prop_conv.convert(step.cond_expr);
@@ -519,12 +562,23 @@ void symex_target_equationt::convert_goto_instructions(
 void symex_target_equationt::convert_constraints(
   decision_proceduret &decision_procedure) const
 {
+  const unsigned verbosity =
+    decision_procedure.get_message_handler().get_verbosity();
+  const bool debug_output = verbosity >= messaget::M_DEBUG;
+
   for(const auto &step : SSA_steps)
   {
     if(step.is_constraint())
     {
       if(!step.ignore)
       {
+        if(debug_output)
+        {
+          std::ostringstream oss;
+          step.output(oss);
+          decision_procedure.debug() << oss.str() << messaget::eom;
+        }
+
         try
         {
           decision_procedure.set_to_true(step.cond_expr);