utop # #require "z3";;
─( 14:40:42 )─< command 1 >──────────────────────────────────────────────────────────────────────────────────────────────{ counter: 0 }─
utop # let ctx=Z3.mk_context  [("model", "true"); ("proof", "false")] ;;
val ctx : Z3.context = <abstr>
─( 14:40:47 )─< command 2 >──────────────────────────────────────────────────────────────────────────────────────────────{ counter: 0 }─
utop # let abs1=Z3.SMT.parse_smtlib2_string ctx
                "(define-fun abs ((x Int)) Int
                (ite (>= x 0) x (- x)))" [] [] [] [];;
Exception: Z3.Error("parser error").
Raised by primitive operation at unknown location
Called from file "//toplevel//", line 1, characters 9-141
Called from file "toplevel/toploop.ml", line 180, characters 17-56