diff --git a/sidekick-bin.opam b/sidekick-bin.opam
index 888c8091..26e8bfdf 100644
--- a/sidekick-bin.opam
+++ b/sidekick-bin.opam
@@ -15,11 +15,15 @@ depends: [
   "containers"
   "iter"
   "zarith"
+  "smtlib-utils" { >= "0.1" & < "0.2" }
   "sidekick" { = version }
   "menhir"
   "msat" { >= "0.8" < "0.9" }
   "ocaml" { >= "4.03" } 
 ]
+pin-depends: [
+  ["smtlib-utils.0.1" "git+https://github.com/c-cube/smtlib-utils.git"]
+]
 tags: [ "sat" "smt" ]
 homepage: "https://github.com/c-cube/sidekick"
 dev-repo: "git+https://github.com/c-cube/sidekick.git"
diff --git a/src/smtlib/Lexer.mll b/src/smtlib/Lexer.mll
deleted file mode 100644
index 72d7b7cd..00000000
--- a/src/smtlib/Lexer.mll
+++ /dev/null
@@ -1,95 +0,0 @@
-
-(* This file is free software. See file "license" for more details. *)
-
-(** {1 Lexer for TIP} *)
-
-{
-  module A = Parse_ast
-  module Loc = Locations
-  open Parser (* for tokens *)
-
-}
-
-let printable_char = [^ '\n']
-let comment_line = ';' printable_char*
-
-let sym = [^ '"' '(' ')' '\\' ' ' '\t' '\r' '\n']
-
-let ident = sym+
-
-let quoted = '"' ([^ '"'] | '\\' '"')* '"'
-let escaped = '|' [^ '|']* '|'
-
-rule token = parse
-  | eof { EOI }
-  | '\n' { Lexing.new_line lexbuf; token lexbuf }
-  | [' ' '\t' '\r'] { token lexbuf }
-  | comment_line { token lexbuf }
-  | '(' { LEFT_PAREN }
-  | ')' { RIGHT_PAREN }
-  | "true" { TRUE }
-  | "false" { FALSE }
-  | "or" { OR }
-  | "and" { AND }
-  | "not" { NOT }
-  | "xor" { XOR }
-  | "distinct" { DISTINCT }
-  | "ite" { IF }
-  | "as" { AS }
-  | "match" { MATCH }
-  | "case" { CASE }
-  | "default" { DEFAULT }
-  | "lambda" { FUN }
-  | "let" { LET }
-  | "par" { PAR }
-  | "=>" { ARROW }
-  | "=" { EQ }
-  | "@" { AT }
-  | "+" { ADD }
-  | "-" { MINUS }
-  | "*" { PROD }
-  | "/" { DIV }
-  | "<=" { LEQ }
-  | "<" { LT }
-  | ">=" { GEQ }
-  | ">" { GT }
-  | "declare-datatypes" { DATA }
-  | "assert" { ASSERT }
-  | "lemma" { LEMMA }
-  | "assert-not" { ASSERT_NOT }
-  | "declare-sort" { DECLARE_SORT }
-  | "declare-fun" { DECLARE_FUN }
-  | "declare-const" { DECLARE_CONST }
-  | "define-fun" { DEFINE_FUN }
-  | "define-fun-rec" { DEFINE_FUN_REC }
-  | "define-funs-rec" { DEFINE_FUNS_REC }
-  | "forall" { FORALL }
-  | "exists" { EXISTS }
-  | "check-sat" { CHECK_SAT }
-  | "set-logic" { SET_LOGIC }
-  | "set-option" { SET_OPTION }
-  | "set-info" { SET_INFO }
-  | "exit" { EXIT }
-  | ident {
-    let s = Lexing.lexeme lexbuf in
-    IDENT(s)
-  }
-  | quoted {
-      (* TODO: unescape *)
-      let s = Lexing.lexeme lexbuf in
-      let s = String.sub s 1 (String.length s -2) in (* remove " " *)
-      QUOTED s }
-  | escaped {
-      let s = Lexing.lexeme lexbuf in
-      CCString.iter (function '\n' -> Lexing.new_line lexbuf | _ -> ()) s;
-      let s = String.sub s 1 (String.length s -2) in (* remove "|" *)
-      ESCAPED s }
-  | _ as c
-    {
-      let loc = Loc.of_lexbuf lexbuf in
-      A.parse_errorf ~loc "unexpected char '%c'" c
-    }
-
-{
-
-}
diff --git a/src/smtlib/Locations.ml b/src/smtlib/Locations.ml
deleted file mode 100644
index bf5368e7..00000000
--- a/src/smtlib/Locations.ml
+++ /dev/null
@@ -1,70 +0,0 @@
-(* This file is free software, copyright Simon Cruanes. See file "LICENSE" for more details. *)
-
-(** {1 Locations} *)
-
-type t = {
-  file : string;
-  start_line : int;
-  start_column : int;
-  stop_line : int;
-  stop_column : int;
-}
-
-let mk file start_line start_column stop_line stop_column =
-  { file; start_line; start_column; stop_line; stop_column; }
-
-let mk_pair file (a,b)(c,d) = mk file a b c d
-
-let mk_pos start stop =
-  let open Lexing in
-  mk
-    start.pos_fname
-    start.pos_lnum (start.pos_cnum - start.pos_bol)
-    stop.pos_lnum (stop.pos_cnum - stop.pos_bol)
-
-let equal = (=)
-
-let pp out pos =
-  if pos.start_line = pos.stop_line
-  then
-    Format.fprintf out "file '%s': line %d, col %d to %d"
-      pos.file pos.start_line pos.start_column pos.stop_column
-  else
-    Format.fprintf out "file '%s': line %d, col %d to line %d, col %d"
-      pos.file
-      pos.start_line pos.start_column
-      pos.stop_line pos.stop_column
-
-let pp_opt out = function
-  | None -> Format.fprintf out "<no location>"
-  | Some pos -> pp out pos
-
-let pp_to_string pp x =
-  let buf = Buffer.create 64 in
-  let fmt = Format.formatter_of_buffer buf in
-  pp fmt x;
-  Format.pp_print_flush fmt ();
-  Buffer.contents buf
-
-let to_string_opt = pp_to_string pp_opt
-
-(** {2 Lexbuf} *)
-
-let set_file buf filename =
-  let open Lexing in
-  buf.lex_curr_p <- {buf.lex_curr_p with pos_fname=filename;};
-  ()
-
-let get_file buf =
-  let open Lexing in
-  buf.lex_curr_p.pos_fname
-
-let of_lexbuf lexbuf =
-  let start = Lexing.lexeme_start_p lexbuf in
-  let end_ = Lexing.lexeme_end_p lexbuf in
-  let s_l = start.Lexing.pos_lnum in
-  let s_c = start.Lexing.pos_cnum - start.Lexing.pos_bol in
-  let e_l = end_.Lexing.pos_lnum in
-  let e_c = end_.Lexing.pos_cnum - end_.Lexing.pos_bol in
-  let file = get_file lexbuf in
-  mk file s_l s_c e_l e_c
diff --git a/src/smtlib/Parse_ast.ml b/src/smtlib/Parse_ast.ml
deleted file mode 100644
index 821730dc..00000000
--- a/src/smtlib/Parse_ast.ml
+++ /dev/null
@@ -1,294 +0,0 @@
-
-(* This file is free software. See file "license" for more details. *)
-
-(** {1 Simple AST for parsing} *)
-
-module Loc = Locations
-module Fmt = CCFormat
-
-let pp_str = Format.pp_print_string
-
-let pp_to_string pp x =
-  let buf = Buffer.create 64 in
-  let fmt = Format.formatter_of_buffer buf in
-  pp fmt x;
-  Format.pp_print_flush fmt ();
-  Buffer.contents buf
-
-type var = string
-type ty_var = string
-
-(** Polymorphic types *)
-type ty =
-  | Ty_bool
-  | Ty_app of ty_var * ty list
-  | Ty_arrow of ty list * ty
-
-type typed_var = var * ty
-
-type arith_op =
-  | Leq
-  | Lt
-  | Geq
-  | Gt
-  | Add
-  | Minus
-  | Mult
-  | Div
-
-(** {2 AST: S-expressions with locations} *)
-type term =
-  | True
-  | False
-  | Const of string
-  | Arith of arith_op * term list
-  | App of string * term list
-  | HO_app of term * term (* higher-order application *)
-  | Match of term * match_branch list
-  | If of term * term * term
-  | Let of (var * term) list * term
-  | Fun of typed_var * term
-  | Eq of term * term
-  | Imply of term * term
-  | And of term list
-  | Or of term list
-  | Not of term
-  | Xor of term * term
-  | Distinct of term list
-  | Cast of term * ty (* type cast *)
-  | Forall of (var * ty) list * term
-  | Exists of (var * ty) list * term
-
-and match_branch =
-  | Match_default of term
-  | Match_case of string * var list * term
-
-type cstor = {
-  cstor_name: string;
-  cstor_args: (string * ty) list; (* selector+type *)
-}
-
-type 'arg fun_decl = {
-  fun_ty_vars: ty_var list;
-  fun_name: string;
-  fun_args: 'arg list;
-  fun_ret: ty;
-}
-
-type fun_def = {
-  fr_decl: typed_var fun_decl;
-  fr_body: term;
-}
-
-type funs_rec_def = {
-  fsr_decls: typed_var fun_decl list;
-  fsr_bodies: term list;
-}
-
-type statement = {
-  stmt: stmt;
-  loc: Loc.t option;
-}
-
-and stmt =
-  | Stmt_decl_sort of string * int (* arity *)
-  | Stmt_decl of ty fun_decl
-  | Stmt_fun_def of fun_def
-  | Stmt_fun_rec of fun_def
-  | Stmt_funs_rec of funs_rec_def
-  | Stmt_data of ty_var list * (string * cstor list) list
-  | Stmt_assert of term
-  | Stmt_lemma of term
-  | Stmt_assert_not of ty_var list * term
-  | Stmt_set_logic of string
-  | Stmt_set_option of string list
-  | Stmt_set_info of string list
-  | Stmt_check_sat
-  | Stmt_exit
-
-let ty_bool = Ty_bool
-let ty_app s l = Ty_app (s,l)
-let ty_const s = ty_app s []
-let ty_arrow_l args ret = if args=[] then ret else Ty_arrow (args, ret)
-let ty_arrow a b = ty_arrow_l [a] b
-
-let true_ = True
-let false_ = False
-let const s = Const s
-let app f l = App (f,l)
-let ho_app a b = HO_app (a,b)
-let ho_app_l a l = List.fold_left ho_app a l
-let match_ u l = Match (u,l)
-let if_ a b c = If(a,b,c)
-let fun_ v t = Fun (v,t)
-let fun_l = List.fold_right fun_
-let let_ l t = Let (l,t)
-let eq a b = Eq (a,b)
-let imply a b = Imply(a,b)
-let xor a b = Xor (a,b)
-let and_ l = And l
-let or_ l = Or l
-let distinct l = Distinct l
-let cast t ~ty = Cast (t, ty)
-let forall vars f = match vars with [] -> f | _ -> Forall (vars, f)
-let exists vars f = match vars with [] -> f | _ -> Exists (vars, f)
-let rec not_ t = match t with
-  | Forall (vars,u) -> exists vars (not_ u)
-  | Exists (vars,u) -> forall vars (not_ u)
-  | _ -> Not t
-
-let arith op l = Arith (op,l)
-
-let _mk ?loc stmt = { loc; stmt }
-
-let mk_cstor name l : cstor = { cstor_name=name; cstor_args=l }
-let mk_fun_decl ~ty_vars f args ret =
-  { fun_ty_vars=ty_vars; fun_name=f;
-    fun_args=args; fun_ret=ret; }
-let mk_fun_rec ~ty_vars f args ret body =
-  { fr_decl=mk_fun_decl ~ty_vars f args ret; fr_body=body; }
-
-let decl_sort ?loc s ~arity = _mk ?loc (Stmt_decl_sort (s, arity))
-let decl_fun ?loc ~tyvars f ty_args ty_ret =
-  let d = {fun_ty_vars=tyvars; fun_name=f; fun_args=ty_args; fun_ret=ty_ret} in
-  _mk ?loc (Stmt_decl d)
-let fun_def ?loc fr = _mk ?loc (Stmt_fun_def fr)
-let fun_rec ?loc fr = _mk ?loc (Stmt_fun_rec fr)
-let funs_rec ?loc decls bodies = _mk ?loc (Stmt_funs_rec {fsr_decls=decls; fsr_bodies=bodies})
-let data ?loc tyvars l = _mk ?loc (Stmt_data (tyvars,l))
-let assert_ ?loc t = _mk ?loc (Stmt_assert t)
-let lemma ?loc t = _mk ?loc (Stmt_lemma t)
-let assert_not ?loc ~ty_vars t = _mk ?loc (Stmt_assert_not (ty_vars, t))
-let set_logic ?loc s = _mk ?loc (Stmt_set_logic s)
-let set_option ?loc l = _mk ?loc (Stmt_set_option l)
-let set_info ?loc l = _mk ?loc (Stmt_set_info l)
-let check_sat ?loc () = _mk ?loc Stmt_check_sat
-let exit ?loc () = _mk ?loc Stmt_exit
-
-let loc t = t.loc
-let view t = t.stmt
-
-let fpf = Format.fprintf
-
-
-let pp_tyvar = pp_str
-
-let rec pp_ty out (ty:ty) = match ty with
-  | Ty_bool -> pp_str out "Bool"
-  | Ty_app (s,[]) -> pp_str out s
-  | Ty_app (s,l) -> Format.fprintf out "(@[<hv1>%s@ %a@])" s (Util.pp_list pp_ty) l
-  | Ty_arrow (args,ret) ->
-    fpf out "(@[=>@ %a@ %a@])" (Util.pp_list pp_ty) args pp_ty ret
-
-let pp_arith out = function
-  | Leq -> Fmt.string out "<="
-  | Lt -> Fmt.string out "<"
-  | Geq -> Fmt.string out ">="
-  | Gt -> Fmt.string out ">"
-  | Add -> Fmt.string out "+"
-  | Minus -> Fmt.string out "-"
-  | Mult -> Fmt.string out "*"
-  | Div -> Fmt.string out "/"
-
-let rec pp_term out (t:term) = match t with
-  | True -> pp_str out "true"
-  | False -> pp_str out "false"
-  | Arith (op,l) ->
-    Fmt.fprintf out "(@[<hv>%a@ %a@])" pp_arith op (Util.pp_list pp_term) l
-  | Const s -> pp_str out s
-  | App (f,l) -> fpf out "(@[<1>%s@ %a@])" f (Util.pp_list pp_term) l
-  | HO_app (a,b) -> fpf out "(@[<1>@@@ %a@ %a@])" pp_term a pp_term b
-  | Match (lhs,cases) ->
-    let pp_case out = function
-      | Match_default rhs -> fpf out "(@[<1>case default@ %a@])" pp_term rhs
-      | Match_case (c,[],rhs) ->
-        fpf out "(@[<1>case %s@ %a@])" c pp_term rhs
-      | Match_case (c,vars,rhs) ->
-        fpf out "(@[<1>case@ (@[%s@ %a@])@ %a@])" c (Util.pp_list pp_str) vars pp_term rhs
-    in
-    fpf out "(@[<1>match@ %a@ @[<v>%a@]@])" pp_term lhs
-      (Util.pp_list pp_case) cases
-  | If (a,b,c) -> fpf out "(@[<hv1>ite %a@ %a@ %a@])" pp_term a pp_term b pp_term c
-  | Fun (v,body) -> fpf out "(@[<1>lambda @ (%a)@ %a@])" pp_typed_var v pp_term body
-  | Let (l,t) ->
-    let pp_binding out (v,t) = fpf out "(@[%s@ %a@])" v pp_term t in
-    fpf out "(@[let@ (@[%a@])@ %a@])" (Util.pp_list pp_binding) l pp_term t
-  | Eq (a,b) -> fpf out "(@[=@ %a@ %a@])" pp_term a pp_term b
-  | Imply (a,b) -> fpf out "(@[=>@ %a@ %a@])" pp_term a pp_term b
-  | Xor(a,b) -> fpf out "(@[xor@ %a@ %a@])" pp_term a pp_term b
-  | And l -> fpf out "(@[<hv>and@ %a@])" (Util.pp_list pp_term) l
-  | Or l -> fpf out "(@[<hv>or@ %a@])" (Util.pp_list pp_term) l
-  | Not t -> fpf out "(not %a)" pp_term t
-  | Distinct l -> fpf out "(@[distinct@ %a@])" (Util.pp_list pp_term) l
-  | Cast (t, ty) -> fpf out "(@[<hv1>as@ @[%a@]@ @[%a@]@])" pp_term t pp_ty ty
-  | Forall (vars,f) ->
-    fpf out "(@[<hv1>forall@ (@[%a@])@ %a@])" (Util.pp_list pp_typed_var) vars pp_term f
-  | Exists (vars,f) ->
-    fpf out "(@[<hv1>exists@ (@[%a@])@ %a@])" (Util.pp_list pp_typed_var) vars pp_term f
-and pp_typed_var out (v,ty) =
-  fpf out "(@[%s@ %a@])" v pp_ty ty
-
-let pp_par pp_x out (ty_vars,x) = match ty_vars with
-  | [] -> pp_x out x
-  | _ ->
-    fpf out "(@[<1>par (@[%a@])@ (%a)@])" (Util.pp_list pp_tyvar) ty_vars pp_x x
-
-let pp_fun_decl pp_arg out fd =
-  fpf out "%s@ (@[%a@])@ %a"
-    fd.fun_name (Util.pp_list pp_arg) fd.fun_args pp_ty fd.fun_ret
-
-let pp_fr out fr =
-  fpf out "@[<1>%a@ %a@]" (pp_fun_decl pp_typed_var) fr.fr_decl pp_term fr.fr_body
-
-let pp_stmt out (st:statement) = match view st with
-  | Stmt_set_logic s -> fpf out "(@[declare-logic@ %s@])" s
-  | Stmt_set_option l -> fpf out "(@[set-option@ %a@])" (Util.pp_list CCFormat.string) l
-  | Stmt_set_info l -> fpf out "(@[set-info@ %a@])" (Util.pp_list CCFormat.string) l
-  | Stmt_decl_sort (s,n) -> fpf out "(@[declare-sort@ %s %d@])" s n
-  | Stmt_assert t -> fpf out "(@[assert@ %a@])" pp_term t
-  | Stmt_lemma t -> fpf out "(@[lemma@ %a@])" pp_term t
-  | Stmt_assert_not (ty_vars,t) ->
-    fpf out "(@[assert-not@ %a@])" (pp_par pp_term) (ty_vars,t)
-  | Stmt_decl d ->
-    fpf out "(@[declare-fun@ %a@])"
-      (pp_par (pp_fun_decl pp_ty)) (d.fun_ty_vars,d)
-  | Stmt_fun_def fr ->
-    fpf out "(@[<1>define-fun@ %a@])"
-      (pp_par pp_fr) (fr.fr_decl.fun_ty_vars, fr)
-  | Stmt_fun_rec fr ->
-    fpf out "(@[<1>define-fun-rec@ %a@])"
-      (pp_par pp_fr) (fr.fr_decl.fun_ty_vars, fr)
-  | Stmt_funs_rec fsr ->
-    let pp_decl' out d = fpf out "(@[<1>%a@])" (pp_fun_decl pp_typed_var) d in
-    fpf out "(@[<hv1>define-funs-rec@ (@[<v>%a@])@ (@[<v>%a@])@])"
-      (Util.pp_list pp_decl') fsr.fsr_decls (Util.pp_list pp_term) fsr.fsr_bodies
-  | Stmt_data (tyvars,l) ->
-    let pp_cstor_arg out (sel,ty) = fpf out "(@[%s %a@])" sel pp_ty ty in
-    let pp_cstor out c =
-      if c.cstor_args = []
-      then fpf out "(%s)" c.cstor_name
-      else fpf out "(@[<1>%s@ %a@])" c.cstor_name (Util.pp_list pp_cstor_arg) c.cstor_args
-    in
-    let pp_data out (s,cstors) =
-      fpf out "(@[<1>%s@ @[<v>%a@]@])" s (Util.pp_list pp_cstor) cstors
-    in
-    fpf out "(@[<hv1>declare-datatypes@ (@[%a@])@ (@[<v>%a@])@])"
-      (Util.pp_list pp_tyvar) tyvars (Util.pp_list pp_data) l
-  | Stmt_check_sat -> pp_str out "(check-sat)"
-  | Stmt_exit -> pp_str out "(exit)"
-
-(** {2 Errors} *)
-
-exception Parse_error of Loc.t option * string
-
-let () = Printexc.register_printer
-    (function
-      | Parse_error (loc, msg) ->
-        let pp out () =
-          Format.fprintf out "parse error at %a:@ %s" Loc.pp_opt loc msg
-        in
-        Some (pp_to_string pp ())
-      | _ -> None)
-
-let parse_error ?loc msg = raise (Parse_error (loc, msg))
-let parse_errorf ?loc msg = Format.ksprintf (parse_error ?loc) msg
diff --git a/src/smtlib/Parser.mly b/src/smtlib/Parser.mly
deleted file mode 100644
index df5e193b..00000000
--- a/src/smtlib/Parser.mly
+++ /dev/null
@@ -1,377 +0,0 @@
-
-
-(* This file is free software, part of tip-parser. See file "license" for more details. *)
-
-(** {1 Parser for TIP} *)
-
-(* vim:SyntasticToggleMode:
-   vim:set ft=yacc: *)
-
-%{
-  module A = Parse_ast
-  module Loc = Locations
-
-%}
-
-%token EOI
-
-%token LEFT_PAREN
-%token RIGHT_PAREN
-
-%token PAR
-%token ARROW
-
-%token TRUE
-%token FALSE
-%token OR
-%token AND
-%token XOR
-%token DISTINCT
-%token NOT
-%token EQ
-%token IF
-%token MATCH
-%token CASE
-%token DEFAULT
-%token FUN
-%token LET
-%token AS
-%token AT
-
-%token LEQ
-%token LT
-%token GEQ
-%token GT
-%token ADD
-%token MINUS
-%token PROD
-%token DIV
-
-%token SET_LOGIC
-%token SET_OPTION
-%token SET_INFO
-%token DATA
-%token ASSERT
-%token LEMMA
-%token ASSERT_NOT
-%token FORALL
-%token EXISTS
-%token DECLARE_SORT
-%token DECLARE_CONST
-%token DECLARE_FUN
-%token DEFINE_FUN
-%token DEFINE_FUN_REC
-%token DEFINE_FUNS_REC
-%token CHECK_SAT
-%token EXIT
-
-%token <string>IDENT
-%token <string>QUOTED
-%token <string>ESCAPED
-
-%start <Parse_ast.term> parse_term
-%start <Parse_ast.ty> parse_ty
-%start <Parse_ast.statement> parse
-%start <Parse_ast.statement list> parse_list
-
-%%
-
-parse_list: l=stmt* EOI {l}
-parse: t=stmt EOI { t }
-parse_term: t=term EOI { t }
-parse_ty: t=ty EOI { t }
-
-cstor_arg:
-  | LEFT_PAREN name=id ty=ty RIGHT_PAREN { name, ty }
-
-cstor:
-  | LEFT_PAREN c=id RIGHT_PAREN { A.mk_cstor c [] }
-  | LEFT_PAREN c=id l=cstor_arg+ RIGHT_PAREN
-    { A.mk_cstor c l }
-
-data:
-  | LEFT_PAREN s=id l=cstor+ RIGHT_PAREN { s,l }
-
-fun_def_mono:
-  | f=id
-    LEFT_PAREN args=typed_var* RIGHT_PAREN
-    ret=ty
-    { f, args, ret }
-
-fun_decl_mono:
-  | f=id
-    LEFT_PAREN args=ty* RIGHT_PAREN
-    ret=ty
-    { f, args, ret }
-
-fun_decl:
-  | tup=fun_decl_mono { let f, args, ret = tup in [], f, args, ret }
-  | LEFT_PAREN
-      PAR
-      LEFT_PAREN tyvars=tyvar* RIGHT_PAREN
-      LEFT_PAREN tup=fun_decl_mono RIGHT_PAREN
-    RIGHT_PAREN
-    { let f, args, ret = tup in tyvars, f, args, ret }
-
-fun_rec:
-  | tup=fun_def_mono body=term
-    {
-      let f, args, ret = tup in
-      A.mk_fun_rec ~ty_vars:[] f args ret body
-    }
-  | LEFT_PAREN
-      PAR
-      LEFT_PAREN l=tyvar* RIGHT_PAREN
-      LEFT_PAREN tup=fun_def_mono body=term RIGHT_PAREN
-    RIGHT_PAREN
-    {
-      let f, args, ret = tup in
-      A.mk_fun_rec ~ty_vars:l f args ret body
-    }
-
-funs_rec_decl:
-  | LEFT_PAREN tup=fun_def_mono RIGHT_PAREN
-    {
-      let f, args, ret = tup in
-      A.mk_fun_decl ~ty_vars:[] f args ret
-    }
-  | LEFT_PAREN
-      PAR
-      LEFT_PAREN l=tyvar* RIGHT_PAREN
-      LEFT_PAREN tup=fun_def_mono RIGHT_PAREN
-    RIGHT_PAREN
-    {
-      let f, args, ret = tup in
-      A.mk_fun_decl ~ty_vars:l f args ret
-    }
-
-assert_not:
-  | LEFT_PAREN
-      PAR LEFT_PAREN tyvars=tyvar+ RIGHT_PAREN t=term
-    RIGHT_PAREN
-  { tyvars, t }
-  | t=term
-  { [], t }
-
-id:
-  | s=IDENT { s }
-  | s=QUOTED { s }
-  | s=ESCAPED { s }
-
-stmt:
-  | LEFT_PAREN SET_LOGIC s=id RIGHT_PAREN
-    {
-      let loc = Loc.mk_pos $startpos $endpos in
-      A.set_logic ~loc s
-    }
-  | LEFT_PAREN SET_OPTION l=id+ RIGHT_PAREN
-    {
-      let loc = Loc.mk_pos $startpos $endpos in
-      A.set_option ~loc l
-    }
-  | LEFT_PAREN SET_INFO l=id+ RIGHT_PAREN
-    {
-      let loc = Loc.mk_pos $startpos $endpos in
-      A.set_info ~loc l
-    }
-  | LEFT_PAREN ASSERT t=term RIGHT_PAREN
-    {
-      let loc = Loc.mk_pos $startpos $endpos in
-      A.assert_ ~loc t
-    }
-  | LEFT_PAREN LEMMA t=term RIGHT_PAREN
-    {
-      let loc = Loc.mk_pos $startpos $endpos in
-      A.lemma ~loc t
-    }
-  | LEFT_PAREN DECLARE_SORT s=id n=id RIGHT_PAREN
-    {
-      let loc = Loc.mk_pos $startpos $endpos in
-      try
-        let n = int_of_string n in
-        A.decl_sort ~loc s ~arity:n
-      with Failure _ ->
-        A.parse_errorf ~loc "expected arity to be an integer, not `%s`" n
-    }
-  | LEFT_PAREN DATA
-      LEFT_PAREN vars=tyvar* RIGHT_PAREN
-      LEFT_PAREN l=data+ RIGHT_PAREN
-    RIGHT_PAREN
-    {
-      let loc = Loc.mk_pos $startpos $endpos in
-      A.data ~loc vars l
-    }
-  | LEFT_PAREN DECLARE_FUN tup=fun_decl RIGHT_PAREN
-    {
-      let loc = Loc.mk_pos $startpos $endpos in
-      let tyvars, f, args, ret = tup in
-      A.decl_fun ~loc ~tyvars f args ret
-    }
-  | LEFT_PAREN DECLARE_CONST f=id ty=ty RIGHT_PAREN
-    {
-      let loc = Loc.mk_pos $startpos $endpos in
-      A.decl_fun ~loc ~tyvars:[] f [] ty
-    }
-  | LEFT_PAREN DEFINE_FUN f=fun_rec RIGHT_PAREN
-    {
-      let loc = Loc.mk_pos $startpos $endpos in
-      A.fun_def ~loc f
-    }
-  | LEFT_PAREN
-    DEFINE_FUN_REC
-    f=fun_rec
-    RIGHT_PAREN
-    {
-      let loc = Loc.mk_pos $startpos $endpos in
-      A.fun_rec ~loc f
-    }
-  | LEFT_PAREN
-    DEFINE_FUNS_REC
-      LEFT_PAREN decls=funs_rec_decl+ RIGHT_PAREN
-      LEFT_PAREN bodies=term+ RIGHT_PAREN
-    RIGHT_PAREN
-    {
-      let loc = Loc.mk_pos $startpos $endpos in
-      A.funs_rec ~loc decls bodies
-    }
-  | LEFT_PAREN
-    ASSERT_NOT
-    tup=assert_not
-    RIGHT_PAREN
-    {
-      let loc = Loc.mk_pos $startpos $endpos in
-      let ty_vars, f = tup in
-      A.assert_not ~loc ~ty_vars f
-    }
-  | LEFT_PAREN CHECK_SAT RIGHT_PAREN
-    {
-      let loc = Loc.mk_pos $startpos $endpos in
-      A.check_sat ~loc ()
-    }
-  | LEFT_PAREN EXIT RIGHT_PAREN
-    {
-      let loc = Loc.mk_pos $startpos $endpos in
-      A.exit ~loc ()
-    }
-  | error
-    {
-      let loc = Loc.mk_pos $startpos $endpos in
-      A.parse_errorf ~loc "expected statement"
-    }
-
-var:
-  | s=id { s }
-tyvar:
-  | s=id { s }
-
-ty:
-  | s=id {
-    begin match s with
-      | "Bool" -> A.ty_bool
-      | _ -> A.ty_const s
-    end
-    }
-  | LEFT_PAREN s=id args=ty+ RIGHT_PAREN
-    { A.ty_app s args }
-  | LEFT_PAREN ARROW tup=ty_arrow_args RIGHT_PAREN
-    {
-      let args, ret = tup in
-      A.ty_arrow_l args ret }
-  | error
-    {
-      let loc = Loc.mk_pos $startpos $endpos in
-      A.parse_errorf ~loc "expected type"
-    }
-
-ty_arrow_args:
-  | a=ty ret=ty { [a], ret }
-  | a=ty tup=ty_arrow_args { a :: fst tup, snd tup }
-
-typed_var:
-  | LEFT_PAREN s=id ty=ty RIGHT_PAREN { s, ty }
-
-case:
-  | LEFT_PAREN
-      CASE
-      c=id
-      rhs=term
-    RIGHT_PAREN
-    { A.Match_case (c, [], rhs) }
-  | LEFT_PAREN
-      CASE
-      LEFT_PAREN c=id vars=var+ RIGHT_PAREN
-      rhs=term
-    RIGHT_PAREN
-    { A.Match_case (c, vars, rhs) }
-  | LEFT_PAREN
-     CASE DEFAULT rhs=term
-    RIGHT_PAREN
-    { A.Match_default rhs }
-
-binding:
-  | LEFT_PAREN v=var t=term RIGHT_PAREN { v, t }
-
-term:
-  | TRUE { A.true_ }
-  | FALSE { A.false_ }
-  | s=id { A.const s }
-  | t=composite_term { t }
-  | error
-    {
-      let loc = Loc.mk_pos $startpos $endpos in
-      A.parse_errorf ~loc "expected term"
-    }
-
-%inline arith_op:
-  | ADD { A.Add }
-  | MINUS { A.Minus }
-  | PROD { A.Mult }
-  | DIV { A.Div }
-  | LEQ { A.Leq }
-  | LT { A.Lt }
-  | GEQ { A.Geq }
-  | GT { A.Gt }
-
-composite_term:
-  | LEFT_PAREN IF a=term b=term c=term RIGHT_PAREN { A.if_ a b c }
-  | LEFT_PAREN OR l=term+ RIGHT_PAREN { A.or_ l }
-  | LEFT_PAREN AND l=term+ RIGHT_PAREN { A.and_ l }
-  | LEFT_PAREN NOT t=term RIGHT_PAREN { A.not_ t }
-  | LEFT_PAREN DISTINCT l=term+ RIGHT_PAREN { A.distinct l }
-  | LEFT_PAREN EQ a=term b=term RIGHT_PAREN { A.eq a b }
-  | LEFT_PAREN ARROW a=term b=term RIGHT_PAREN { A.imply a b }
-  | LEFT_PAREN XOR a=term b=term RIGHT_PAREN { A.xor a b }
-  | LEFT_PAREN f=id args=term+ RIGHT_PAREN { A.app f args }
-  | LEFT_PAREN o=arith_op args=term+ RIGHT_PAREN { A.arith o args }
-  | LEFT_PAREN f=composite_term args=term+ RIGHT_PAREN { A.ho_app_l f args }
-  | LEFT_PAREN AT f=term arg=term RIGHT_PAREN { A.ho_app f arg }
-  | LEFT_PAREN
-      MATCH
-      lhs=term
-      l=case+
-    RIGHT_PAREN
-    { A.match_ lhs l }
-  | LEFT_PAREN
-      FUN
-      LEFT_PAREN vars=typed_var+ RIGHT_PAREN
-      body=term
-    RIGHT_PAREN
-    { A.fun_l vars body }
-  | LEFT_PAREN
-      LET
-      LEFT_PAREN l=binding+ RIGHT_PAREN
-      r=term
-    RIGHT_PAREN
-    { A.let_ l r }
-  | LEFT_PAREN AS t=term ty=ty RIGHT_PAREN
-    { A.cast t ~ty }
-  | LEFT_PAREN FORALL LEFT_PAREN vars=typed_var+ RIGHT_PAREN
-    f=term
-    RIGHT_PAREN
-    { A.forall vars f }
-  | LEFT_PAREN EXISTS LEFT_PAREN vars=typed_var+ RIGHT_PAREN
-    f=term
-    RIGHT_PAREN
-    { A.exists vars f }
-
-%%
diff --git a/src/smtlib/Sidekick_smtlib.ml b/src/smtlib/Sidekick_smtlib.ml
index 474a64e4..1359cc4f 100644
--- a/src/smtlib/Sidekick_smtlib.ml
+++ b/src/smtlib/Sidekick_smtlib.ml
@@ -4,7 +4,8 @@ module ID = Sidekick_base_term.ID
 module Fmt = CCFormat
 module Ast = Ast
 module E = CCResult
-module Loc = Locations
+module Loc = Smtlib_utils.Loc
+module Parse_ast = Smtlib_utils.Ast
 module Process = Process
 module Solver = Process.Solver
 
@@ -19,7 +20,7 @@ module Parse = struct
   let parse_chan_exn ?(filename="<no name>") ic =
     let lexbuf = Lexing.from_channel ic in
     Loc.set_file lexbuf filename;
-    Parser.parse_list Lexer.token lexbuf
+    Smtlib_utils.Parser.parse_list Smtlib_utils.Lexer.token lexbuf
 
   let parse_file_exn file : Parse_ast.statement list =
     CCIO.with_in file (parse_chan_exn ~filename:file)
diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml
index 9a691b7d..01e0e638 100644
--- a/src/smtlib/Typecheck.ml
+++ b/src/smtlib/Typecheck.ml
@@ -3,12 +3,12 @@
 (** {1 Preprocessing AST} *)
 
 open Sidekick_base_term
-module Loc = Locations
+module Loc = Smtlib_utils.Loc
 module Fmt = CCFormat
 module Log = Msat.Log
 
 module A = Ast
-module PA = Parse_ast
+module PA = Smtlib_utils.Ast
 
 type 'a or_error = ('a, string) CCResult.t
 
@@ -118,6 +118,7 @@ let find_id_ ctx (s:string): ID.t =
 (* parse a type *)
 let rec conv_ty ctx (t:PA.ty) : A.Ty.t * _ = match t with
   | PA.Ty_bool -> A.Ty.prop, Ctx.K_ty Ctx.K_bool
+  | PA.Ty_real -> A.Ty.rat, Ctx.K_ty Ctx.K_other
   | PA.Ty_app ("Rat",[]) -> A.Ty.rat, Ctx.K_ty Ctx.K_other
   | PA.Ty_app ("Int",[]) -> A.Ty.int , Ctx.K_ty Ctx.K_other
   | PA.Ty_app (f, l) ->
@@ -211,10 +212,6 @@ let rec conv_term ctx (t:PA.term) : A.term = match t with
     let a = conv_term ctx a in
     let b = conv_term ctx b in
     A.imply a b
-  | PA.Xor (a,b) ->
-    let a = conv_term ctx a in
-    let b = conv_term ctx b in
-    A.or_ (A.and_ a (A.not_ b)) (A.and_ (A.not_ a) b)
   | PA.Match (lhs, l) ->
     (*
     errorf_ctx ctx "TODO: support match in %a" PA.pp_term t
@@ -363,7 +360,7 @@ let rec conv_statement ctx (s:PA.statement): A.statement list =
 and conv_statement_aux ctx (stmt:PA.statement) : A.statement list = match PA.view stmt with
   | PA.Stmt_set_logic s -> [A.SetLogic s]
   | PA.Stmt_set_option l -> [A.SetOption l]
-  | PA.Stmt_set_info l -> [A.SetInfo l]
+  | PA.Stmt_set_info (a,b) -> [A.SetInfo [a;b]]
   | PA.Stmt_exit -> [A.Exit]
   | PA.Stmt_decl_sort (s,n) ->
     let id = Ctx.add_id ctx s (Ctx.K_ty Ctx.K_uninterpreted) in
@@ -442,14 +439,5 @@ and conv_statement_aux ctx (stmt:PA.statement) : A.statement list = match PA.vie
     let t = conv_term ctx t in
     check_bool_ t;
     [A.Assert t]
-  | PA.Stmt_assert_not ([], t) ->
-    let vars, t = A.unfold_binder A.Forall (conv_term ctx t) in
-    let g = A.not_ t in (* negate *)
-    [A.Goal (vars, g)]
-  | PA.Stmt_assert_not (_::_, _) ->
-    errorf_ctx ctx "cannot convert polymorphic goal@ `@[%a@]`"
-      PA.pp_stmt stmt
-  | PA.Stmt_lemma _ ->
-    errorf_ctx ctx "smbc does not know how to handle `lemma` statements"
   | PA.Stmt_check_sat -> [A.CheckSat]
 
diff --git a/src/smtlib/Typecheck.mli b/src/smtlib/Typecheck.mli
index 9bd19de8..bb5c46e5 100644
--- a/src/smtlib/Typecheck.mli
+++ b/src/smtlib/Typecheck.mli
@@ -2,7 +2,7 @@
 
 (** {1 Preprocessing AST} *)
 
-module Loc = Locations
+module Loc = Smtlib_utils.Loc
 
 type 'a or_error = ('a, string) CCResult.t
 
@@ -14,7 +14,7 @@ module Ctx : sig
   val pp : t CCFormat.printer
 end
 
-module PA = Parse_ast
+module PA = Smtlib_utils.Ast
 module A = Ast
 
 val conv_term : Ctx.t -> PA.term -> A.term
diff --git a/src/smtlib/dune b/src/smtlib/dune
index 2ee60601..8666bf3c 100644
--- a/src/smtlib/dune
+++ b/src/smtlib/dune
@@ -3,11 +3,5 @@
  (public_name sidekick-bin.smtlib)
  (libraries containers zarith msat sidekick.core sidekick.util
    sidekick.msat-solver sidekick.base-term sidekick.th-bool-static
-   sidekick.mini-cc msat.backend)
+   sidekick.mini-cc msat.backend smtlib-utils)
  (flags :standard -open Sidekick_util))
-
-(menhir
- (modules Parser))
-
-(ocamllex
- (modules Lexer))