Die OCaml-Bibliothek von Z3 löst einen Segmentierungsfehler aus

Question

Betrachten Sie das folgende OCaml-Code-Snippet, das das Z3-Modul als Schnittstelle zum Z3-Solver verwendet. Der Code versucht, einen neuen TPair Datentyp in Z3 mit einem einzigen Konstruktor zu definieren T, die zwei Integer-Argumente akzeptiert:

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 

Die Anrufe get_tester_decl und get_accessor_decls beiden Wurfsegmentierungsfehler. Was könnte der Grund sein?

Answer 1

Kein Code, der in reinem OCaml geschrieben wurde, kann einen Segmentierungsfehler verursachen. Dies liegt daran, dass OCaml eine speicherfreundliche Sprache ist. Das Problem liegt irgendwo in der Installation, entweder an der Stelle, an der OCaml an die darunterliegende Bibliothek gebunden ist, oder in der z3-Bibliothek selbst.

Nur Autoren von Bibliotheken (oder Bindungen) können Ihnen beim Debuggen und Beheben dieses Problems behilflich sein. Bitte erstellen Sie ein Problem in the upstream Repository.