GOTO trace: no timestamps for single-threaded programs

Avoid reading clock values when those won't be known to the solver as
single-threaded source programs do not have partial-order constraints.
Other back-ends were silent about this, but the incremental SMT back-end
produced warnings (which the user could do nothing about).

Author: tautschnig

src/goto-symex/build_goto_trace.cpp

@@ -220,6 +220,7 @@ void build_goto_trace(
   time_mapt time_map;
 
   mp_integer current_time=0;
+  bool has_threads = target.has_threads();
 
   ssa_step_iteratort last_step_to_keep = target.SSA_steps.end();
   bool last_step_was_kept = false;
@@ -258,6 +259,9 @@ void build_goto_trace(
     else if(it->is_shared_read() || it->is_shared_write() ||
             it->is_atomic_end())
     {
+      if(!has_threads)
+        continue;
+
       mp_integer time_before=current_time;
 
       if(it->is_shared_read() || it->is_shared_write())

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -477,20 +477,6 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
   }();
   if(!descriptor)
   {
-    if(const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(expr))
-    {
-      // Note this case is currently expected to be encountered during trace
-      // generation for -
-      //  * Steps which were removed via --slice-formula.
-      //  * Getting concurrency clock values.
-      // The below implementation which returns the given expression was chosen
-      // based on the implementation of `smt2_convt::get` in the non-incremental
-      // smt2 decision procedure.
-      log.warning()
-        << "`get` attempted for unknown symbol, with identifier - \n"
-        << symbol_expr->get_identifier() << messaget::eom;
-      return expr;
-    }
     return build_expr_based_on_getting_operands(expr, *this);
   }
   if(const auto array_type = type_try_dynamic_cast<array_typet>(expr.type()))

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -505,26 +505,6 @@ TEST_CASE(
         test.sent_commands ==
         std::vector<smt_commandt>{smt_get_value_commandt{foo_term}});
     }
-    SECTION("Get value of non-set symbol")
-    {
-      // smt2_incremental_decision_proceduret is used this way when cbmc is
-      // invoked with the combination of `--trace` and `--slice-formula`.
-      test.sent_commands.clear();
-      const exprt bar =
-        make_test_symbol("bar", signedbv_typet{16}).symbol_expr();
-      REQUIRE(test.procedure.get(bar) == bar);
-      REQUIRE(test.sent_commands.empty());
-    }
-    SECTION("Get value of type less symbol back")
-    {
-      // smt2_incremental_decision_proceduret is used this way as part of
-      // building the goto trace, to get the partial order concurrency clock
-      // values.
-      test.sent_commands.clear();
-      const symbol_exprt baz = symbol_exprt::typeless("baz");
-      REQUIRE(test.procedure.get(baz) == baz);
-      REQUIRE(test.sent_commands.empty());
-    }
     SECTION("Get value of trivially solved expression")
     {
       test.sent_commands.clear();