Klee与STP与Klee和其他SAT求解器

Question

klee使用STP作为约束求解器，但是从理论上讲，可以更改其求解器。STP不允许浮点操作。如果我们决定用另一个约束求解器替换STP，例如Z3，Klee是否能够生成浮点约束？

流是：C代码 -> LLVM比特码 -> Klee-> STP子句 -> klee->输出

如果Klee获取浮点LLVM指令，是否可以解释它们？它是否以SMT语言生成FP约束，STP无法处理它们，或者根本不会生成FP约束？

您答案的任何参考都将不胜感激。

Answer 1

此链接包含带有浮点支撑的klee叉。不知道它有多成熟。