3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-13 12:25:37 +00:00

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.
This commit is contained in:
Eric Astor 2026-06-10 18:13:05 -04:00 committed by GitHub
parent 384414b10c
commit 677abb589e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -3,6 +3,7 @@ def_module_params('fp',
export=True,
params=(('engine', SYMBOL, 'auto-config',
'Select: auto-config, datalog, bmc, spacer'),
('rlimit', UINT, 0, "deterministic resource limit (0 means no limit)"),
('datalog.default_table', SYMBOL, 'sparse',
'default table implementation: sparse, hashtable, bitvector, interval'),
('datalog.default_relation', SYMBOL, 'pentagon',