是否有可能改变使用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;
