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

@@ -436,36 +436,21 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
   }();
   if(!descriptor)
   {
-    if(gather_dependent_expressions(expr).empty())
-    {
-      INVARIANT(
-        objects_are_already_tracked(expr, object_map),
-        "Objects in expressions being read should already be tracked from "
-        "point of being set/handled.");
-      descriptor = ::convert_expr_to_smt(
-        expr,
-        object_map,
-        pointer_sizes_map,
-        object_size_function.make_application,
-        is_dynamic_object_function.make_application);
-    }
-    else
-    {
-      const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(expr);
-      INVARIANT(
-        symbol_expr, "Unhandled expressions are expected to be symbols");
-      // 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;
-    }
+    INVARIANT_WITH_DIAGNOSTICS(
+      gather_dependent_expressions(expr).empty(),
+      "Unhandled expression",
+      irep_pretty_diagnosticst{expr});
+
+    INVARIANT(
+      objects_are_already_tracked(expr, object_map),
+      "Objects in expressions being read should already be tracked from "
+      "point of being set/handled.");
+    descriptor = ::convert_expr_to_smt(
+      expr,
+      object_map,
+      pointer_sizes_map,
+      object_size_function.make_application,
+      is_dynamic_object_function.make_application);
   }
   if(const auto array_type = type_try_dynamic_cast<array_typet>(expr.type()))
   {

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -510,26 +510,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();
@@ -542,16 +522,6 @@ TEST_CASE(
         test.sent_commands ==
         std::vector<smt_commandt>{smt_get_value_commandt{not_true_term}});
     }
-    SECTION("Invariant violated due to expression in unexpected form.")
-    {
-      const mult_exprt unexpected{foo.symbol_expr(), from_integer(2, foo.type)};
-      const cbmc_invariants_should_throwt invariants_throw;
-      REQUIRE_THROWS_MATCHES(
-        test.procedure.get(unexpected),
-        invariant_failedt,
-        invariant_failure_containing(
-          "Unhandled expressions are expected to be symbols"));
-    }
     SECTION("Error handling of mismatched response.")
     {
       test.sent_commands.clear();