我正在尝试设计方法来改善我的问题的z3性能。我知道CAV'06 paper和tech report。 z3 v4.3.1的相关部分是否与这些文档中描述的内容有所不同，如果有什么不同？另外，z3中默认用于决定何时检查线性实算术中与所确定的（和传播的）命题文字相对应的理论原子的一致性的策略是什么？
线性算术在src/smt/theory_arith*的文件中实现。参见http://z3.codeplex.com/SourceControl/latest#src/smt/theory_arith_core.h
关于您所指出的论文，这些想法在实现中使用。但是，实际代码包含许多扩展，可用于线性整数，非线性算术和证明生成。如果仅关心线性实数运算，则应仅关注theory_arith.h，theory_arith_core.h。文件theory_arith_aux.h也包含有用的功能。