我使用Z3_solver非线性实际运算。 我也想为解算超时。 我使用下面的代码，但它看起来像，由于求解永远运行超时不起作用。 谁能帮我找到了问题？
Z3_solver solver;
cfg = Z3_mk_config();
ctx = Z3_mk_context(cfg);
Z3_symbol logic_symbol = Z3_mk_string_symbol(ctx, "QF_UFNRA");
solver = Z3_mk_solver_for_logic((Z3_context)ctx, logic_symbol);
Z3_solver_inc_ref(ctx, solver);
Z3_params params = Z3_mk_params(ctx);
Z3_params_inc_ref(ctx, params);
Z3_symbol r = Z3_mk_string_symbol(ctx, ":timeout");
Z3_params_set_uint(ctx, params, r, 10);
Z3_solver_set_params(ctx, solver, params);
Z3_params_dec_ref(ctx, params);
Z3_del_config(cfg);
....
Z3_solver_assert(ctx,solver,pred);
Z3_lbool b = Z3_solver_check(ctx, solver);
你在Linux或FreeBSD使用Z3？ 我最近固定，影响这两个系统的定时器的设定问题（承诺： http://z3.codeplex.com/SourceControl/changeset/9674f511b3c1 ）
此修复程序已经可以在“工作进行中”分支。 您可以使用检索
git clone https://git01.codeplex.com/z3 -b unstable
我测试了它使用下面的python脚本。 顺便说一句，如果你发现与“不稳定”分支问题，请报告。
from z3 import *
a1, a2, t1, t2 = Reals('a1 a2 t1 t2');
s = SolverFor("QF_NRA")
s.add( a1 + a2 == 2,
a1*t1 + a2*t2 == Q(2,3),
a1*t1*t1 + a2*t2*t2 == Q(2,5),
a1*t1*t1*t1 + a2*t2*t2*t2 == Q(2,7) )
# On my machine, I get unknown when I set the timeout to 1ms.
s.set(timeout=1)
print s.check()
编辑：下面是关于如何打造Z3指示unstable分支（又名“工作进行中”分支）：
假设：我们将会把Z3源代码目录~/code ，且我们将不进行全系统的安装。
cd ~
mkdir -p code
cd code
git clone https://git01.codeplex.com/z3 -b unstable
cd z3
python scripts/mk_make.py
cd build
make
顺便说一句，如果你有一个多核心机，可以加快使用编译步骤
make -j N
代替
make
其中N是在你的机器的内核数量。
