From cf620504d9b23e769be783d8fbfe653562006d3d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 28 Mar 2026 20:06:42 +0000
Subject: [PATCH] Handle empty type in incremental SMT2 decision procedure

Skip symbols and nondet symbols with empty_typet (void) in
gather_dependent_expressions to avoid attempting SMT sort conversion.
Add early return in send_function_definition for empty-typed
expressions as a defensive measure. Handle equality over empty type
in set_to by treating it as vacuously true, matching the behavior
of the non-incremental SMT2 backend.

Remove no-new-smt exclusion tag from havoc_slice_checks and
memset_null regression tests since they now pass with the
incremental SMT2 backend.

Fixes: #8077
---
 regression/cbmc/havoc_slice_checks/test.desc    |  2 +-
 regression/cbmc/memset_null/test.desc           |  2 +-
 .../smt2_incremental_decision_procedure.cpp     | 17 ++++++++++++++++-
 3 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/regression/cbmc/havoc_slice_checks/test.desc b/regression/cbmc/havoc_slice_checks/test.desc
index 42b6f11e2c3..b5d12522d0a 100644
--- a/regression/cbmc/havoc_slice_checks/test.desc
+++ b/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$
diff --git a/regression/cbmc/memset_null/test.desc b/regression/cbmc/memset_null/test.desc
index 6984ae9e29d..bef94363c5e 100644
--- a/regression/cbmc/memset_null/test.desc
+++ b/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$
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 0d8a91a6f89..aa0829e2483 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/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);