CODEWITHSUNDEEP
ocamlz3
Gowtham Kaki
Gowtham Kaki

Reputation: 377

Z3's OCaml library throws segmentation fault

Consider the following OCaml code snippet that uses Z3 module to interface with the Z3 solver. The code tries to define a new TPair datatype in Z3 with a single constructor T that accepts two integer arguments:

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

The calls to get_tester_decl and get_accessor_decls both throw segmentation fault. What could be the reason?

Upvotes: 0

Views: 146

Answers (1)

ivg
ivg

Reputation: 35210

No code, written in pure OCaml, can cause a segmentation fault. This is because OCaml is a memory safe language. The problem is somewhere in the plumbing, either in the place where OCaml is bound to the underlying library, on in the z3 library itself.

Only library (or bindings) authors can help you in debugging and fixing this issue. So please, create an issue in the upstream repository.

Upvotes: 1

Related Questions