Improve coverage of incr-oneloop traces

by adding a test for the standard trace and comment out the non-standard ones
for now.

Author: petr-bauch

regression/cbmc-incr-oneloop/alarm2/trace_test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--incremental-loop main.0 --unwind-min 5 --unwind-max 10 --trace
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^State \d+ file main.c function havocIO line 501 thread \d+$
+--
+^warning: ignoring

src/goto-checker/single_loop_incremental_symex_checker.cpp

@@ -168,25 +168,33 @@ operator()(propertiest &properties)
 
 goto_tracet single_loop_incremental_symex_checkert::build_full_trace() const
 {
-  goto_tracet goto_trace;
-  build_goto_trace(
-    equation,
-    equation.SSA_steps.end(),
-    property_decider.get_decision_procedure(),
-    ns,
-    goto_trace);
-
-  return goto_trace;
+  UNREACHABLE;
+  // When needed un-comment the implementation below, right now `cover` and
+  // `paths` are incompatible.
+  //
+  // goto_tracet goto_trace;
+  // build_goto_trace(
+  //   equation,
+  //   equation.SSA_steps.end(),
+  //   property_decider.get_decision_procedure(),
+  //   ns,
+  //   goto_trace);
+
+  // return goto_trace;
 }
 
 goto_tracet single_loop_incremental_symex_checkert::build_shortest_trace() const
 {
   if(options.get_bool_option("beautify"))
   {
-    // NOLINTNEXTLINE(whitespace/braces)
-    counterexample_beautificationt{ui_message_handler}(
-      dynamic_cast<boolbvt &>(property_decider.get_stack_decision_procedure()),
-      equation);
+    UNREACHABLE;
+    // For now, beautification and incremental are incompatible.
+    //
+    // auto &decision_procedure = dynamic_cast<boolbvt &>(
+    //   property_decider.get_stack_decision_procedure());
+    // auto counterexample_beautification =
+    //   counterexample_beautificationt{ui_message_handler};
+    // counterexample_beautification(decision_procedure, equation);
   }
 
   goto_tracet goto_trace;