Z3 C API 在运行时更改超时

是否可以使用 C API 在运行时更改求解器的超时值？ 为了设置超时，可以执行以下操作 -

Z3_config  cfg = Z3_mk_config();
Z3_set_param_value(cfg, "SOFT_TIMEOUT", "10000") // set timeout to 10 seconds
Z3_context ctx = Z3_mk_context(cfg);
....
Z3_check_and_get_model(ctx);
....
....
Z3_check_and_get_model(ctx);

但是，假设我们想在保留上下文的同时更改下一个查询的超时，是否可以更改其间的超时值？

考虑迁移到 Z3 4.0。 Z3 4.0 具有新的 API，允许用户在同一 Z3_context 中创建多个求解器。您可以为每个求解器设置不同的超时，并随时更新它们。 Z3 4.0还附带了C++层，使C API的使用更加方便。 这是一个设置超时的简短示例。在我的机器上，Z3将会返回unknown当使用 1 毫秒超时时，并且sat当。。。的时候s.set(p)命令被删除。

context c;
expr x = c.real_const("x");
expr y = c.real_const("y");
solver s(c);

s.add(x >= 1);
s.add(y < x + 3);

params p(c);
p.set(":timeout", static_cast<unsigned>(1)); // in milliseconds
s.set(p);

std::cout << s.check() << std::endl;