make assumption output in trace reachable

Assumptions are never violated, instead they restrict the search space for non-det values

Author: polgreen

regression/cbmc/multiple-goto-traces/test.desc

@@ -5,7 +5,7 @@ activate-multi-line-match
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
-Trace for main\.assertion\.1:(\n.*){16}  assertion 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:(\n.*){30}  assertion argc != 4(\n.*){5}Trace for main\.assertion\.4:(\n.*){44}  assertion argc \+ 1 != 5
+Trace for main\.assertion\.1:(\n.*){22}  assertion 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:(\n.*){36}  assertion argc != 4(\n.*){5}Trace for main\.assertion\.4:(\n.*){50}  assertion argc \+ 1 != 5
 \*\* 3 of 4 failed
 --
 ^warning: ignoring

src/goto-programs/goto_trace.cpp

@@ -522,22 +522,16 @@ void show_full_goto_trace(
       break;
 
     case goto_trace_stept::typet::ASSUME:
-      if(!step.cond_value)
+      if(step.cond_value && step.pc->is_assume())
       {
         out << "\n";
         out << "Assumption:\n";
 
         if(!step.pc->source_location.is_nil())
           out << "  " << step.pc->source_location << '\n';
 
-        if(step.pc->is_assume())
-        {
-          out << "  "
-              << from_expr(ns, step.function_id, step.pc->get_condition())
-              << '\n';
-        }
-
-        out << '\n';
+        out << "  " << from_expr(ns, step.function_id, step.pc->get_condition())
+            << '\n';
       }
       break;