Is it possible to change the timeout value of the solver at runtime using C API?
In order to set the timeout the following can be done -
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);
However, suppose we want to change the timeout for next query while retaining the context, is it possible to change the timeout value in between?
Consider moving to Z3 4.0. Z3 4.0 has new API that allows the user to create many solvers in the same Z3_context. You can set different timeouts for each solver, and update them whenever you want. Z3 4.0 also comes with a C++ layer that makes the C API much more convenient to use.
Here is an short example that sets a timeout. On my machine, Z3 will return unknown when the 1 millisecond timeout is used, and sat when the s.set(p) command is removed.
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;
