z3 · Issues· 46 开放

recfun_finder 应在作用域退出时删除递归定义

模型不正确

合并无效的模型错误

我们是否可以在 nuget.org 上发布新版本?

`unsat` 序列基准,现在无法由 z3 处理

MBQI 模型检查器辅助函数 `context::check` 中的 SIGSEGV - 每次运行故障位置不同 (看起来像是状态损坏); 回归, 4.16.0 状态良好

从 4.14.1 升级到 4.15.3 后,计算和内存均出现回退

[解决方案健全性问题] Float32 FP/Real 往返算术中的 SAT 结果不正确。

[合并] 仅适用于小实例（字符串、位向量）

使用固定点求解器时性能回退 (从 4.13.2 到 4.14.1)

在 Spacer 中遇到意外代码

仅在不必要的 assert 条件下为不满足,否则为未知

在处理字符串序列时未知

在不使用 SharedArrayBuffer 或 COOP/COEP 头的情况下, z3-solver 的替代解决方案

从 4.8.7.0 到 4.8.8.0 及之后的所有版本的性能回退。