Z3 中的分段错误 (Haskell)

Question

我正在使用 Haskell 创建一些 Z3 公式。当我尝试运行以下代码时，出现分段错误（尽管我制作的其他示例效果很好）。有人知道这是否是 Z3 中的错误吗？ Haskell 中使用的 API 是 C API 名称的镜像：

{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TupleSections #-}

import Z3.Monad
import Control.Monad.IO.Class
import Control.Applicative
import Data.Traversable
import Prelude hiding (sequence)

main = do
    out <- evalZ3 $ do
        is  <- mkIntSort
        _3  <- mkInteger 3
        _5  <- mkInteger 5
        _10 <- mkInteger 10
        x   <- mkFreshIntVar "x"
        y   <- mkFreshIntVar "y"
        y2  <- mkBvmul y y

        assert =<< mkAnd =<< sequence
            [ mkEq x y2
            ]
        return ()

    print "end"

Answer 1

您真的应该向 Haskell Z3 软件包维护者报告此事；因为他们应该首先防止这种使用。您可以在以下位置找到他们的联系信息：http://hackage.haskell.org/package/z3

Answer 2

这是我们库中的错误。在 4.0.0 中我们引入了自动内存管理，但是我们错过了与错误处理的交互。似乎内存管理代码在错误处理代码之前执行。因此，当 mkBVmul returns 时，内存管理代码尝试增加结果对象的引用计数，结果对象变为 null，然后库才知道是一个错误。

我为此创建了一个问题（参见 https://bitbucket.org/iago/z3-haskell/issues/5/segmentation-fault-due-to-type-error），我会尽快解决它。但我们非常感谢您将来向我们报告分段错误。今天我们不在工作中使用这个库，所以即使我维护它，并且我确实尝试帮助任何想要贡献的人，我主要依靠用户报告错误并贡献补丁。

话虽这么说，一旦错误被修复，您将得到一个 Haskell 异常，错误代码为 Z3_SORT_ERROR。 z3-haskell 绑定几乎不提供类型安全，这是一个设计决定。编写类型安全的 Z3 API 并非易事，需要相当多的类型黑客和一些 GHC 扩展。我们的目标用户是使用 Z3 作为后端的工具编写者。他们中的大多数人不想自己处理编组和内存管理，但仍然希望对 Z3 的 API 进行低级访问。

我们不希望人们直接使用我们的绑定来编写 SMT 问题，sbv 更适合这种情况。当然可以为 z3-haskell 创建一个类型安全的包装器作为一个单独的包。我有这个在我的待办事项列表中，我只是没有找到时间。

Z3 中的分段错误 (Haskell)

Segmentation fault in Z3 (Haskell)

c

haskell

segmentation-fault

z3