Handle empty type in incremental SMT2 decision procedure

regression/cbmc/havoc_slice_checks/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^\[main\.assertion\.\d+\] line 9 assertion havoc_slice W_OK.*: FAILURE$

regression/cbmc/memset_null/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^\[main.precondition_instance.1\] line .* memset destination region writeable: FAILURE$

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -88,7 +88,8 @@ static std::vector<exprt> gather_dependent_expressions(const exprt &root_expr)
       can_cast_expr<nondet_symbol_exprt>(expr_node) ||
       can_cast_expr<string_constantt>(expr_node))
     {
-      dependent_expressions.push_back(expr_node);
+      if(expr_node.type().id() != ID_empty)
+        dependent_expressions.push_back(expr_node);
     }
     // The decision procedure does not depend on the values inside address of
     // code typed expressions. We can build the address without knowing the
@@ -170,6 +171,10 @@ void send_function_definition(
     &expression_identifiers,
   std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
 {
+  // The empty type (void) has no SMT representation, so we do not
+  // declare functions for symbols of this type.
+  if(expr.type().id() == ID_empty)
+    return;
   const smt_declare_function_commandt function{
     smt_identifier_termt(
       symbol_identifier, convert_type_to_smt_sort(expr.type())),
@@ -616,6 +621,16 @@ void smt2_incremental_decision_proceduret::set_to(
           << in_expr.pretty(2, 0) << messaget::eom;
   });
   const exprt lowered_expr = lower(in_expr);
+  // Equality over empty (void) type expressions is vacuously true,
+  // matching the behavior of the non-incremental SMT2 backend.
+  if(
+    lowered_expr.id() == ID_equal &&
+    to_equal_expr(lowered_expr).lhs().type().id() == ID_empty)
+  {
+    if(!value)
+      solver_process->send(smt_assert_commandt{smt_bool_literal_termt{false}});
+    return;
+  }
   PRECONDITION(can_cast_type<bool_typet>(lowered_expr.type()));
 
   define_dependent_functions(lowered_expr);