GOTO trace: no timestamps for single-threaded programs

[tautschnig]

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).

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Base: 78.39% // Head: 78.40% // Increases project coverage by +0.00% 🎉

Coverage data is based on head (f1a830b) compared to base (b03d870).
Patch coverage: 100.00% of modified lines in pull request are covered.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #7403   +/-   ##
========================================
  Coverage    78.39%   78.40%           
========================================
  Files         1655     1655           
  Lines       190281   190275    -6     
========================================
+ Hits        149172   149178    +6     
+ Misses       41109    41097   -12     

Impacted Files	Coverage Δ
src/goto-symex/build_goto_trace.cpp	87.08% <100.00%> (-0.79%)	⬇️
...ncremental/smt2_incremental_decision_procedure.cpp	96.63% <100.00%> (-0.05%)	⬇️
...ncremental/smt2_incremental_decision_procedure.cpp	98.57% <100.00%> (-0.02%)	⬇️
src/solvers/smt2/smt2_conv.cpp	68.63% <0.00%> (-0.04%)	⬇️
src/util/irep.cpp	99.49% <0.00%> (+1.52%)	⬆️
src/util/irep.h	97.97% <0.00%> (+2.02%)	⬆️
src/util/invariant.cpp	80.39% <0.00%> (+7.84%)	⬆️
src/util/invariant.h	95.55% <0.00%> (+13.33%)	⬆️

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

[thomasspriggs]

I am happy to see updates to the trace building such that the calls it makes to the decision procedure are more consistent. However it looks like the changes to smt2_incremental_decision_proceduret in this PR will conflict with those in #7404

I haven't done an in-depth review of this PR yet, this is just an initial comment.

[tautschnig]

I am happy to see updates to the trace building such that the calls it makes to the decision procedure are more consistent. However it looks like the changes to smt2_incremental_decision_proceduret in this PR will conflict with those in #7404

I noticed the same when looking at #7404 - I'm more than happy for #7404 to land first, and I'll rebase this one on top of it.

[tautschnig]

I am happy to see updates to the trace building such that the calls it makes to the decision procedure are more consistent. However it looks like the changes to smt2_incremental_decision_proceduret in this PR will conflict with those in #7404

I noticed the same when looking at #7404 - I'm more than happy for #7404 to land first, and I'll rebase this one on top of it.

Rebased.