3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-08 06:52:26 +00:00

seq_regex: fix ill-formed lambda capture that breaks the build on master (#10401)

`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
This commit is contained in:
Margus Veanes 2026-08-04 20:09:23 -07:00 committed by GitHub
parent 227238cc0c
commit ae29ceb6a8
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -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) {