Implement symbol_exprt to smt_termt conversion

Author: thomasspriggs

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -46,8 +46,8 @@ smt_sortt convert_type_to_smt_sort(const typet &type)
 
 static smt_termt convert_expr_to_smt(const symbol_exprt &symbol_expr)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for symbol expression: " + symbol_expr.pretty());
+  return smt_identifier_termt{symbol_expr.get_identifier(),
+                              convert_type_to_smt_sort(symbol_expr.type())};
 }
 
 static smt_termt convert_expr_to_smt(const nondet_symbol_exprt &nondet_symbol)

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -34,6 +34,13 @@ TEST_CASE("\"typet\" to smt sort conversion", "[core][smt2_incremental]")
   }
 }
 
+TEST_CASE("\"symbol_exprt\" to smt term conversion", "[core][smt2_incremental]")
+{
+  CHECK(
+    convert_expr_to_smt(symbol_exprt{"foo", bool_typet{}}) ==
+    smt_identifier_termt("foo", smt_bool_sortt{}));
+}
+
 TEST_CASE(
   "\"exprt\" to smt term conversion for constants/literals",
   "[core][smt2_incremental]")