From 677abb589e931fcbf97c275e18f8eb41da281bbd Mon Sep 17 00:00:00 2001 From: Eric Astor Date: Wed, 10 Jun 2026 18:13:05 -0400 Subject: [PATCH] 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. --- src/muz/base/fp_params.pyg | 1 + 1 file changed, 1 insertion(+) diff --git a/src/muz/base/fp_params.pyg b/src/muz/base/fp_params.pyg index 57a264768..2dd4cea3f 100644 --- a/src/muz/base/fp_params.pyg +++ b/src/muz/base/fp_params.pyg @@ -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',