Z3のOCamlライブラリがセグメント化エラーをスローする

Question

Z3モジュールを使用してZ3ソルバとインターフェイスする次のOCamlコードスニペットを考えてみましょう。コードは、2つの整数の引数を受け入れ、単一のコンストラクタTとZ3に新しいTPairデータ型を定義しようとします：

open Z3                       
open Z3.SMT 
open Z3.Expr                      
open Z3.Symbol                     
open Z3.Datatype                     
open Z3.FuncDecl 
open Z3.Arithmetic 
open Z3.Arithmetic.Integer                  
open Z3.Quantifier 

let _ =                       
    let cfg = [("model", "true"); ("proof", "false")] in 
    let ctx = (mk_context cfg) in 
    let sym = Symbol.mk_string ctx in 
    let s_Int = mk_sort ctx in 
    (* (declare-datatypes() ((TPair (T Int Int))))*) 
    let s_T = mk_constructor_s ctx "T" (sym "isT") 
       [sym "left"; sym "right"]               
       [Some s_Int; Some s_Int] [0; 0] in            
    let s_TPair = mk_sort_s ctx "TPair" [s_T] in 
    let _::s_content::_ = Constructor.get_accessor_decls s_T in         
    let s_isT = Constructor.get_tester_decl s_T in             
    let solver = Solver.mk_solver ctx None in 
    begin 
     Printf.printf "***** CONTEXT ******\n";             
     print_string @@ Solver.to_string solver; 
     Printf.printf "\n*********************\n" 
    end 

get_tester_declとget_accessor_declsの両方への呼び出しセグメンテーションフォールトをスローします。理由は何でしょうか？

Answer 1

純粋なOCamlで書かれたコードは、セグメンテーション違反を引き起こす可能性があります。これは、OCamlがメモリセーフな言語であるためです。この問題は、配管のどこかで、OCamlが基礎となるライブラリにバインドされている場所か、z3ライブラリ自体のいずれかにあります。

ライブラリ（またはバインディング）の作成者のみが、この問題のデバッグや修正をお手伝いします。ですので、the upstreamリポジトリに問題を作成してください。