From ae29ceb6a8e67ed7f79f0bfa2111c5c9b47367d3 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Tue, 4 Aug 2026 20:09:23 -0700 Subject: [PATCH] seq_regex: fix ill-formed lambda capture that breaks the build on master (#10401) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `master` currently does not compile. The merged version of #10398 replaced the plain loop in `seq_regex::all_true` with ```cpp return all_of(lits, [&ctx](literal lit) { return l_true == ctx.get_assignment(lit); }); ``` `ctx` is a **data member** of `seq_regex` (`seq_regex.cpp:31`), not a variable with automatic storage duration, so naming it in a lambda capture list is ill-formed. All three major compilers reject it: - MSVC: `error C2065: 'ctx': undeclared identifier` - GCC: `error: capture of non-variable 'smt::seq_regex::ctx'` - Clang: `error: 'ctx' in capture list does not name a variable` This changes the capture to `this`, which is what the body actually needs in order to reach `ctx`. The predicate itself is untouched, so there is no behavioural change. Verified: `z3.exe` builds cleanly, and `inputs/issues/iss-9928/instance14703.smt2` — the original soundness reproducer from #10398 — still answers `sat`. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2 --- src/smt/seq_regex.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 96ce5eac8e..0eec49165c 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -99,7 +99,7 @@ namespace smt { } bool seq_regex::all_true(literal_vector const& lits) const { - return all_of(lits, [&ctx](literal lit) { return l_true == ctx.get_assignment(lit); }); + return all_of(lits, [this](literal lit) { return l_true == ctx.get_assignment(lit); }); } void seq_regex::add_core_literal(void* dep, literal_vector& lits) {