goto-symex: handle plain-symbol quantifier bound variables in rewrite_quantifiers

src/goto-symex/goto_symex_state.cpp

@@ -251,8 +251,26 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
     rename<level>(expr.type(), irep_idt(), ns);
 
     // do this recursively
-    Forall_operands(it, expr)
-      *it = rename<level>(std::move(*it), ns).get();
+    // For quantifiers, skip renaming bound variables (operand 0) to prevent
+    // field sensitivity from decomposing struct-typed symbols into struct
+    // expressions, which violates the quantifier invariant.
+    if(expr.id() == ID_forall || expr.id() == ID_exists)
+    {
+      PRECONDITION(expr.operands().size() == 2);
+      for(auto &bv : expr.operands()[0].operands())
+        rename<level>(bv.type(), irep_idt(), ns);
+      // Rename body without field sensitivity by temporarily disabling it
+      auto saved = field_sensitivity.enabled;
+      field_sensitivity.enabled = false;
+      expr.operands()[1] =
+        rename<level>(std::move(expr.operands()[1]), ns).get();
+      field_sensitivity.enabled = saved;
+    }
+    else
+    {
+      Forall_operands(it, expr)
+        *it = rename<level>(std::move(*it), ns).get();
+    }
 
     const exprt &c_expr = as_const(expr);
 
@@ -290,8 +308,10 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
       c_expr.type().pretty(),
       to_if_expr(c_expr).false_case().type().pretty());
 
-    if(level == L2)
+    if(level == L2 && field_sensitivity.enabled)
+    {
       expr = field_sensitivity.apply(ns, *this, std::move(expr), false);
+    }
 
     return renamedt<exprt, level>{std::move(expr)};
   }

src/goto-symex/symex_main.cpp

@@ -260,8 +260,13 @@ void goto_symext::rewrite_quantifiers(exprt &expr, statet &state)
     // for assumptions we can rewrite "exists X. P" to "P"
     // we keep the quantified variable unique by means of L2 renaming
     auto &quant_expr = to_quantifier_expr(expr);
+    // The bound variable may be a plain symbol (e.g. from front ends other than
+    // C, such as Strata) rather than an already-renamed SSA expression; only
+    // unwrap via to_ssa_expr when it really is one.
+    const symbol_exprt &qsym = quant_expr.symbol();
     symbol_exprt tmp0 =
-      to_symbol_expr(to_ssa_expr(quant_expr.symbol()).get_original_expr());
+      is_ssa_expr(qsym) ? to_symbol_expr(to_ssa_expr(qsym).get_original_expr())
+                        : qsym;
     symex_decl(state, tmp0);
     instruction_local_symbols.push_back(tmp0);
     exprt tmp = quant_expr.where();

src/util/simplify_expr.cpp

@@ -2985,6 +2985,20 @@ simplify_exprt::simplify_node_preorder(const exprt &expr)
   {
     result = simplify_unary_pointer_predicate_preorder(to_unary_expr(expr));
   }
+  else if(expr.id() == ID_forall || expr.id() == ID_exists)
+  {
+    // Only simplify the body (operand 1), not the bound variables (operand 0).
+    // Simplifying bound variable symbols would break the quantifier invariant
+    // that requires them to remain symbols.
+    PRECONDITION(expr.operands().size() == 2);
+    auto r_body = simplify_rec(expr.operands()[1]);
+    if(r_body.has_changed())
+    {
+      result.expr = expr;
+      result.expr.operands()[1] = std::move(r_body.expr);
+      result.expr_changed = resultt<>::CHANGED;
+    }
+  }
   else if(expr.has_operands())
   {
     std::optional<exprt::operandst> new_operands;