분할 오류

Question

나는 (하스켈의 외국인 함수 인터페이스를 통해, 그리고 사용한다) 밀접하게 거울이 Z3 패키지와 함께 C API를 하스켈을 사용하고 있습니다 : https://hackage.haskell.org/package/z3

나는 세그먼트 오류를 ​​얻고을

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.

미리 도움을 청하십시오!

Answer 1

붙여 넣은 코드에 간격 문제가 하나 있음을 알 수 있습니다 (맞춤은 do). 그렇지 않으면 문제의 원인이되는 코드인지 확인하십시오.

나는 당신의 문제를 재현 할 수 없습니까 :

% ghc so.hs -fforce-recomp && ./so 2>&1 | tail ; ghc --version ; z3 -version 
[1 of 1] Compiling Main    (so.hs, so.o) 
Linking so ... 
Sat 
Sat 
Sat 
Sat 
Sat 
Sat 
Sat 
Sat 
Sat 
[] 
The Glorious Glasgow Haskell Compilation System, version 7.10.3 
Z3 version 4.4.1 

아, 그리고 :

% ghc-pkg list z3 
    z3-4.1.0 

편집 : 일치 GHC 및 Z3 버전을하고 난 여전히 문제를 재현 할 수

% LD_LIBRARY_PATH=$HOME/lib ghc so.hs -fforce-recomp && LD_LIBRARY_PATH=$HOME/lib ./so 2>&1 | tail ; ghc --version ; z3 -version 
[1 of 1] Compiling Main    (so.hs, so.o) 
Linking so ... 
Sat 
Sat 
Sat 
Sat 
Sat 
Sat 
Sat 
Sat 
Sat 
[] 
The Glorious Glasgow Haskell Compilation System, version 8.0.1 
Z3 version 4.3.2 

을