Add the unimplemented exprs to INVARIANT messages

For ease of seeing what the unimplemented expression is.

Author: thomasspriggs

regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc

@@ -4,8 +4,14 @@ test.c
 Passing problem to incremental SMT2 solving via "z3"
 ^EXIT=(0|127|134|137)$
 ^SIGNAL=0$
+identifier: main::1::x
 --
+type: pointer
 --
 Test that running cbmc with the `--incremental-smt2-solver` argument causes the
 incremental smt2 solving to be used. Note that at the time of adding this test,
 an invariant violation is expected due to the unimplemented solving.
+Regexes matching the printing in the expected failed invariant are included in
+order to test that `--slice-formula` is causing the first unimplemented
+expression passed to `smt2_incremental_decision_proceduret` to relate to the
+variable `x` in function `main` and not to `cprover_initialise`.

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -17,14 +17,13 @@ exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
 
 exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
 {
-  UNIMPLEMENTED;
-  return exprt();
+  UNIMPLEMENTED_FEATURE("`get` of:\n  " + expr.pretty(2, 0));
 }
 
 void smt2_incremental_decision_proceduret::print_assignment(
   std::ostream &out) const
 {
-  UNIMPLEMENTED;
+  UNIMPLEMENTED_FEATURE("printing of assignments.");
 }
 
 std::string
@@ -41,28 +40,34 @@ smt2_incremental_decision_proceduret::get_number_of_solver_calls() const
 
 void smt2_incremental_decision_proceduret::set_to(const exprt &expr, bool value)
 {
-  UNIMPLEMENTED;
+  UNIMPLEMENTED_FEATURE(
+    "`set_to` (" + std::string{value ? "true" : "false"} + "):\n  " +
+    expr.pretty(2, 0));
 }
 
 void smt2_incremental_decision_proceduret::push(
   const std::vector<exprt> &assumptions)
 {
-  UNIMPLEMENTED;
+  for(const auto &assumption : assumptions)
+  {
+    UNIMPLEMENTED_FEATURE(
+      "pushing of assumption:\n  " + assumption.pretty(2, 0));
+  }
+  UNIMPLEMENTED_FEATURE("`push` of empty assumptions.");
 }
 
 void smt2_incremental_decision_proceduret::push()
 {
-  UNIMPLEMENTED;
+  UNIMPLEMENTED_FEATURE("`push`.");
 }
 
 void smt2_incremental_decision_proceduret::pop()
 {
-  UNIMPLEMENTED;
+  UNIMPLEMENTED_FEATURE("`pop`.");
 }
 
 decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
 {
   ++number_of_solver_calls;
-  UNIMPLEMENTED;
-  return decision_proceduret::resultt::D_SATISFIABLE;
+  UNIMPLEMENTED_FEATURE("solving.");
 }