From abbb3c25450bbb1a905de888b78d7d797220334a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 28 Mar 2026 23:47:32 +0000
Subject: [PATCH] Implement quantifier support for incremental SMT2 decision
 procedure

- Add proper conversion of forall_exprt and exists_exprt to SMT terms
- Implement special handling for quantifier expressions in expression traversal
- Fix tuple conversion INVARIANT violations by processing only quantifier bodies
- Extract and handle bound variables correctly in SMT conversion
- Skip code address expressions to avoid unnecessary conversions

Fixes: #8053
---
 .../smt2_incremental/convert_expr_to_smt.cpp  | 53 +++++++++++++++----
 .../smt2_incremental_decision_procedure.cpp   | 16 ++++++
 2 files changed, 60 insertions(+), 9 deletions(-)

diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
index d5910628470..a2b46212468 100644
--- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
+++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
@@ -1385,16 +1385,36 @@ static smt_termt convert_expr_to_smt(
   const forall_exprt &for_all,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for for all expression: " + for_all.pretty());
+  // Extract the bound variables from the quantifier expression
+  std::vector<smt_identifier_termt> bound_variables;
+  for(const auto &variable : for_all.variables())
+  {
+    bound_variables.push_back(smt_identifier_termt{
+      variable.get_identifier(), convert_type_to_smt_sort(variable.type())});
+  }
+
+  // Get the converted predicate (body) of the quantifier
+  const smt_termt &predicate = converted.at(for_all.where());
+
+  return smt_forall_termt{bound_variables, predicate};
 }
 
 static smt_termt convert_expr_to_smt(
   const exists_exprt &exists,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for exists expression: " + exists.pretty());
+  // Extract the bound variables from the quantifier expression
+  std::vector<smt_identifier_termt> bound_variables;
+  for(const auto &variable : exists.variables())
+  {
+    bound_variables.push_back(smt_identifier_termt{
+      variable.get_identifier(), convert_type_to_smt_sort(variable.type())});
+  }
+
+  // Get the converted predicate (body) of the quantifier
+  const smt_termt &predicate = converted.at(exists.where());
+
+  return smt_exists_termt{bound_variables, predicate};
 }
 
 static smt_termt convert_expr_to_smt(
@@ -1923,8 +1943,21 @@ void filtered_visit_post(
       // do modification of 'top' before pushing in case 'top' isn't stable
       top.operands_pushed = true;
       if(filter(*top.e))
-        for(auto &op : top.e->operands())
-          stack.emplace(&op);
+      {
+        // Special handling for quantifiers - only push body, not bound variables tuple
+        if(
+          can_cast_expr<forall_exprt>(*top.e) ||
+          can_cast_expr<exists_exprt>(*top.e))
+        {
+          const auto &quantifier = static_cast<const binding_exprt &>(*top.e);
+          stack.emplace(&quantifier.where());
+        }
+        else
+        {
+          for(auto &op : top.e->operands())
+            stack.emplace(&op);
+        }
+      }
     }
   }
 }
@@ -1956,14 +1989,16 @@ smt_termt convert_expr_to_smt(
       // Avoiding the conversion side steps a need to convert arbitrary code to
       // SMT terms.
       const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr);
-      if(!address_of)
-        return true;
-      return !can_cast_type<code_typet>(address_of->object().type());
+      if(address_of && can_cast_type<code_typet>(address_of->object().type()))
+        return false;
+
+      return true;
     },
     [&](const exprt &expr) {
       const auto find_result = sub_expression_map.find(expr);
       if(find_result != sub_expression_map.cend())
         return;
+
       smt_termt term = dispatch_expr_to_smt_conversion(
         expr,
         sub_expression_map,
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 0d8a91a6f89..ce5098b4971 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -6,6 +6,7 @@
 #include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/mathematical_expr.h>
 #include <util/range.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
@@ -81,6 +82,7 @@ static std::vector<exprt> gather_dependent_expressions(const exprt &root_expr)
   {
     const exprt &expr_node = *stack.top();
     stack.pop();
+
     if(
       can_cast_expr<symbol_exprt>(expr_node) ||
       can_cast_expr<array_exprt>(expr_node) ||
@@ -98,6 +100,20 @@ static std::vector<exprt> gather_dependent_expressions(const exprt &root_expr)
     const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr_node);
     if(address_of && can_cast_type<code_typet>(address_of->object().type()))
       continue;
+
+    // Special handling for quantifiers - skip bound variables tuple and only
+    // process the body/predicate of the quantifier
+    if(
+      can_cast_expr<forall_exprt>(expr_node) ||
+      can_cast_expr<exists_exprt>(expr_node))
+    {
+      // For quantifier expressions, we only need to process the body (where clause)
+      // The bound variables are handled directly in the conversion
+      const auto &quantifier = static_cast<const binding_exprt &>(expr_node);
+      stack.push(&quantifier.where()); // Only process the body
+      continue;
+    }
+
     for(auto &operand : expr_node.operands())
       stack.push(&operand);
   }