3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-13 12:25:37 +00:00
z3/src
Eric Astor 677abb589e
Add rlimit support in fixedpoint parameters (#9798)
The C++ implementation of the fixedpoint engine (in
z3/src/api/api_datalog.cpp) already attempts to read `rlimit` from its
local parameters:

```c++
unsigned rlimit = to_fixedpoint(d)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
```

However, because `rlimit` was not registered in the public fp parameter
schema (`fp_params.pyg`), any attempt by clients to set it locally via
`Z3_fixedpoint_set_params` was rejected by the Z3 parameter validator
with an "unknown parameter" error.
2026-06-10 15:13:05 -07:00
..
ackermannization Fix off-by-one vulnerabilities: use range-based for on goals; cache loop bound 2026-02-19 22:37:22 +00:00
api Bump shell-quote from 1.7.3 to 1.8.4 in /src/api/js (#9803) 2026-06-10 08:40:36 -07:00
ast Update seq_regex_bisim.h 2026-06-10 15:06:12 -07:00
cmd_context refactor solver to include settable stats 2026-06-07 14:17:38 -07:00
math Avoid invalidated column-cell references in LP pivot paths (#9783) 2026-06-09 07:36:05 -07:00
model disable test in tptp, move to native lambdas 2026-06-02 10:38:51 -07:00
muz Add rlimit support in fixedpoint parameters (#9798) 2026-06-10 15:13:05 -07:00
nlsat making try-for tactic exception resilient on cancelation 2026-04-26 15:58:24 -07:00
opt Fixes necessary to compile z3 included in clang-tidy via FetchContents. (#9768) 2026-06-08 19:44:01 -07:00
params prepare for lambda unfolding in ho-matcher and selectively enable ho matching 2026-05-22 13:25:01 -07:00
parsers Fix off-by-one column after comment lines in SMT2 scanner (#9808) 2026-06-10 06:49:31 -07:00
qe Cleanup thanks to Copilot (#9709) 2026-06-04 10:46:33 -07:00
sat refactor solver to include settable stats 2026-06-07 14:17:38 -07:00
shell Fixes necessary to compile z3 included in clang-tidy via FetchContents. (#9768) 2026-06-08 19:44:01 -07:00
smt Add OP_RE_XOR and union-find bisimulation for ground regex equivalence (#9804) 2026-06-10 14:58:20 -07:00
solver refactor solver to include settable stats 2026-06-07 14:17:38 -07:00
tactic refactor solver to include settable stats 2026-06-07 14:17:38 -07:00
test Fix right-side can_add indexing in sls_seq_plugin edit-distance repair (#9773) 2026-06-08 19:36:14 -07:00
util Handle SIGXCPU like a regular timeout (#9697) 2026-06-03 07:26:38 -07:00
CMakeLists.txt git bindings v1.0 2026-02-18 21:02:25 -08:00