我使用的Haskell这个Z3包,密切镜(和利用的,通过Haskell的外部函数接口)的C API:https://hackage.haskell.org/package/z3分段故障哈斯克尔Z3 API
我得到一个分段错误,并设法将其降低到以下几点:
mainx = do
print =<< intCheck [0..70]
intCheck :: [Int] -> IO [Int]
intCheck [] = return []
intCheck (x:xs) =
do
checking <- evalZ3 $ checkImpact x
print checking
return =<< intCheck xs
checkImpact :: Int -> Z3 Result
checkImpact r = do
reset
xSymb <- mkStringSymbol "x"
x <- mkConst xSymb =<< mkIntSort
trace ("asserting = " ++ show r) assert =<< mkEq x x
solverCheck
输出是:
asserting = 0
Sat
asserting = 1
Sat
asserting = 2
Sat
...[omitted]
asserting = 45
Sat
asserting = 46
Segmentation fault: 11
通常情况下,最后断言大约是46的地方,BU它的执行情况各不相同。我最好的猜测是内存没有被正确释放(我无法弄清楚为什么它会在稍微不同的地方停下来),但我不确定这是递归问题(在intCheck中),还是与z3 API。
在此先感谢您的帮助!
我会在haskell软件包中打开一个bug报告,如果出现问题,让他们处理上游问题 – jberryman
我已经完成了tha t: https://bitbucket.org/iago/z3-haskell/issues/12/possible-error-in-package 如果iago在那里回复,而不是在这里,我会发布更新。 – Bill