Z3 的 OCaml 库引发分段错误

Question

考虑以下使用 Z3 模块与 Z3 求解器交互的 OCaml 代码 sn-p。代码尝试在 Z3 中使用一个接受两个整数参数的构造函数 T 定义一个新的 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 存储库中创建一个问题。