diff --git a/Makefile b/Makefile
index 62a73170..cf1b8dfb 100644
--- a/Makefile
+++ b/Makefile
@@ -3,7 +3,7 @@
 LOG=build.log
 COMP=ocamlbuild -log $(LOG) -use-ocamlfind -classic-display
 FLAGS=
-DIRS=-Is sat,smt,util
+DIRS=-Is sat,smt,util,util/smtlib
 DOC=msat.docdir/index.html
 TEST=sat_solve.native
 
diff --git a/sat/sat.ml b/sat/sat.ml
index b1b29bba..265c1c97 100644
--- a/sat/sat.ml
+++ b/sat/sat.ml
@@ -1,22 +1,23 @@
 (* Copyright 2014 Guillaume Bury *)
 
 module Fsat = struct
-  exception Dummy
-  exception Out_of_int
+  exception Dummy of int
 
   (* Until the constant true_ and false_ are not needed anymore,
    * wa can't simply use sigend integers to represent literals *)
   type t = int
 
-  let max_lit = min max_int (- min_int)
+  let max_lit = max_int
+  let max_fresh = ref (-1)
   let max_index = ref 0
 
-  let make i =
-    if i <> 0 then begin
-      max_index := max !max_index (abs i);
-      i
+  let _make i =
+    if i <> 0 && (abs i) < max_lit then begin
+        max_index := max !max_index (abs i);
+        i
     end else
-      raise Dummy
+        (Format.printf "Warning : %d/%d@." i max_lit;
+        raise (Dummy i))
 
   let dummy = 0
 
@@ -31,12 +32,11 @@ module Fsat = struct
   let label a = _str
   let add_label _ _ = ()
 
-  let create, iter =
+  let make i = _make (2 * i)
+  let fresh, iter =
     let create () =
-      if !max_index <> max_lit then
-        (incr max_index; !max_index)
-      else
-        raise Out_of_int
+        incr max_fresh;
+        _make (2 * !max_fresh + 1)
     in
     let iter: (t -> unit) -> unit = fun f ->
       for j = 1 to !max_index do
@@ -45,10 +45,11 @@ module Fsat = struct
     in
     create, iter
 
-  let fresh = create
-
   let print fmt a =
-    Format.fprintf fmt "%s%d" (if a < 0 then "~" else "") (abs a)
+    Format.fprintf fmt "%s%s%d"
+      (if a < 0 then "~" else "")
+      (if a mod 2 = 0 then "v" else "f")
+      ((abs a) / 2)
 
 end
 
@@ -90,14 +91,14 @@ module Make(Dummy : sig end) = struct
 
   let new_atom () =
     try
-      Fsat.create ()
-    with Fsat.Out_of_int ->
+      Fsat.fresh ()
+    with Fsat.Dummy _ ->
       raise Bad_atom
 
   let make i =
     try
       Fsat.make i
-    with Fsat.Dummy ->
+    with Fsat.Dummy _ ->
       raise Bad_atom
 
   let neg = Fsat.neg
diff --git a/sat/tseitin.ml b/sat/tseitin.ml
index ef6acdf5..fb8c95b2 100644
--- a/sat/tseitin.ml
+++ b/sat/tseitin.ml
@@ -44,50 +44,14 @@ module Make (F : Formula_intf.S) = struct
     else if List.mem (make Not [c]) env then Some false
     else None
 
-  (*
-  let rec lift_ite env op l =
-    try
-      let left, (c, t1, t2), right = Term.first_ite l in
-      begin
-        match value env c with
-        | Some true ->
-          lift_ite (c::env) op (left@(t1::right))
-        | Some false ->
-          lift_ite ((make Not [c])::env) op (left@(t2::right))
-        | None ->
-          Comb
-            (And,
-             [Comb
-                (Imp, [c; lift_ite (c::env) op (left@(t1::right))]);
-              Comb (Imp,
-                    [(make Not [c]);
-                     lift_ite
-                       ((make Not [c])::env) op (left@(t2::right))])])
-      end
-    with Not_found ->
-      begin
-        let lit =
-          match op, l with
-          | Eq, [Term.T t1; Term.T t2] ->
-            Literal.Eq (t1, t2)
-          | Neq, ts ->
-            let ts =
-              List.rev_map (function Term.T x -> x | _ -> assert false) ts in
-            Literal.Distinct (false, ts)
-          | Le, [Term.T t1; Term.T t2] ->
-            Literal.Builtin (true, Hstring.make "<=", [t1; t2])
-          | Lt, [Term.T t1; Term.T t2] ->
-            Literal.Builtin (true, Hstring.make "<", [t1; t2])
-          | _ -> assert false
-        in
-        Lit (F.make lit)
-      end
-
-  let make_lit op l = lift_ite [] op l
-  *)
-
   let make_atom p = Lit p
 
+  let atomic_true = F.fresh ()
+  let atomic_false = F.neg atomic_true
+
+  let f_true = make_atom atomic_true
+  let f_false = make_atom atomic_false
+
   let make_not f = make Not [f]
   let make_and l = make And l
   let make_imply f1 f2 = make Imp [f1; f2]
@@ -95,6 +59,11 @@ module Make (F : Formula_intf.S) = struct
   let make_xor f1 f2 = make Or [ make And [ make Not [f1]; f2 ];
                                  make And [ f1; make Not [f2] ] ]
 
+  let make_or = function
+    | [] -> raise Empty_Or
+    | [a] -> a
+    | l -> Comb (Or, l)
+
   (* simplify formula *)
   let rec sform = function
     | Comb (Not, [Lit a]) -> Lit (F.neg a)
@@ -116,15 +85,26 @@ module Make (F : Formula_intf.S) = struct
     | Comb ((Imp | Not), _) -> assert false
     | Lit _ as f -> f
 
+  let rec simplify_clause acc = function
+      | [] -> Some acc
+      | a :: r when F.equal atomic_true a -> None
+      | a :: r when F.equal atomic_false a ->
+              simplify_clause acc r
+      | a :: r -> simplify_clause (a :: acc) r
+
+  let rec rev_opt_map f acc = function
+    | [] -> acc
+    | a :: r -> begin match f a with
+      | None -> rev_opt_map f acc r
+      | Some b -> rev_opt_map f (b :: acc) r
+    end
+
+  let simplify_cnf = rev_opt_map (simplify_clause []) []
 
   let ( @@ ) l1 l2 = List.rev_append l1 l2
   let ( @ ) = `Use_rev_append_instead   (* prevent use of non-tailrec append *)
 
-  let make_or = function
-    | [] -> raise Empty_Or
-    | [a] -> a
-    | l -> Comb (Or, l)
-
+  (*
   let distrib l_and l_or =
     let l =
       if l_or = [] then l_and
@@ -218,18 +198,9 @@ module Make (F : Formula_intf.S) = struct
   let make_cnf f =
     let sfnc = cnf (sform f) in
     init [] sfnc
+  *)
 
   let mk_proxy = F.fresh
-      (*
-    let cpt = ref 0 in
-    fun () ->
-      let t = AETerm.make
-          (Symbols.name (Hstring.make ("PROXY__"^(string_of_int !cpt))))
-          [] Ty.Tbool
-      in
-      incr cpt;
-      F.make (Literal.Eq (t, AETerm.true_))
-      *)
 
   let acc_or = ref []
   let acc_and = ref []
diff --git a/sat/tseitin_intf.ml b/sat/tseitin_intf.ml
index 6f6f8986..5760c79a 100644
--- a/sat/tseitin_intf.ml
+++ b/sat/tseitin_intf.ml
@@ -16,6 +16,9 @@ module type S = sig
   type t
   type atom
 
+  val f_true : t
+  val f_false : t
+
   val make_atom : atom -> t
   (** [make_pred p] builds the atomic formula [p = true].
       @param sign the polarity of the atomic formula *)
@@ -32,6 +35,10 @@ module type S = sig
       list (which is a conjunction) of lists (which are disjunctions) of
       literals. *)
 
+  val simplify_cnf : atom list list -> atom list list
+  (** Simplifies the cnf given as argument : eliminates 'false' atoms, and eliminates clauses
+      with the 'true' atom *)
+
   val print : Format.formatter -> t -> unit
   (** [print fmt f] prints the formula on the formatter [fmt].*)
 
diff --git a/tests/sat/test-002.smt2 b/tests/sat/test-002.smt2
new file mode 100644
index 00000000..e9ee8be4
--- /dev/null
+++ b/tests/sat/test-002.smt2
@@ -0,0 +1,4 @@
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(assert (or a b))
+(check-sat)
diff --git a/tests/unsat/test-000.cnf b/tests/unsat/test-000.cnf
new file mode 100644
index 00000000..dcf4d0c5
--- /dev/null
+++ b/tests/unsat/test-000.cnf
@@ -0,0 +1,5 @@
+c First test
+p cnf 0 0
+1 0
+-1 2 0
+-1 -2 0
diff --git a/tests/unsat/test-003.smt2 b/tests/unsat/test-003.smt2
new file mode 100644
index 00000000..89a49553
--- /dev/null
+++ b/tests/unsat/test-003.smt2
@@ -0,0 +1,4 @@
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(assert (and (or a b) (and (not a) (not b))))
+(check-sat)
diff --git a/tests/unsat/test-004.smt2 b/tests/unsat/test-004.smt2
new file mode 100644
index 00000000..111d2219
--- /dev/null
+++ b/tests/unsat/test-004.smt2
@@ -0,0 +1,4 @@
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(assert (and (or a b) (not a) (not b)))
+(check-sat)
diff --git a/util/.merlin b/util/.merlin
index 9e3a669a..962d669c 100644
--- a/util/.merlin
+++ b/util/.merlin
@@ -1,9 +1,11 @@
 S ./
+S ./smtlib/
 S ../sat/
 S ../common/
 
 B ../_build/
 B ../_build/util/
+B ../_build/util/smtlib/
 B ../_build/sat/
 B ../_build/smt/
 B ../_build/common/
diff --git a/util/parser.ml b/util/parsedimacs.ml
similarity index 100%
rename from util/parser.ml
rename to util/parsedimacs.ml
diff --git a/util/parser.mli b/util/parsedimacs.mli
similarity index 100%
rename from util/parser.mli
rename to util/parsedimacs.mli
diff --git a/util/sat_solve.ml b/util/sat_solve.ml
index 1a049353..71d315f8 100644
--- a/util/sat_solve.ml
+++ b/util/sat_solve.ml
@@ -8,6 +8,7 @@ exception Out_of_space
 (* Types for input/output languages *)
 type sat_input =
   | Dimacs
+  | Smtlib
 
 type sat_output =
   | Standard (* Only output problem status *)
@@ -18,6 +19,7 @@ let output = ref Standard
 
 let input_list = [
   "dimacs", Dimacs;
+  "smtlib", Smtlib;
 ]
 let output_list = [
   "dot", Dot;
@@ -38,8 +40,13 @@ let set_input s = set_io "Input" s input input_list
 let set_output s = set_io "Output" s output output_list
 
 (* Input Parsing *)
+let rec rev_flat_map f acc = function
+    | [] -> acc
+    | a :: r -> rev_flat_map f (List.rev_append (f a) acc) r
+
 let parse_input file = match !input with
-  | Dimacs -> List.rev_map (List.rev_map S.make) (Parser.parse file)
+  | Dimacs -> List.rev_map (List.rev_map S.make) (Parsedimacs.parse file)
+  | Smtlib -> Sat.Tseitin.simplify_cnf (rev_flat_map Sat.Tseitin.make_cnf [] (Smtlib.parse file))
 
 (* Printing wrappers *)
 let std = Format.std_formatter
diff --git a/util/smtlib/.merlin b/util/smtlib/.merlin
new file mode 100644
index 00000000..23ddf6ef
--- /dev/null
+++ b/util/smtlib/.merlin
@@ -0,0 +1,9 @@
+S ./
+S ../
+S ../../sat/
+
+B ../../_build/
+B ../../_build/util/
+B ../../_build/util/smtlib/
+B ../../_build/sat/
+B ../../_build/smt/
diff --git a/util/smtlib/lexsmtlib.mli b/util/smtlib/lexsmtlib.mli
new file mode 100644
index 00000000..a53450a7
--- /dev/null
+++ b/util/smtlib/lexsmtlib.mli
@@ -0,0 +1,3 @@
+(* Copyright 2014 INIA *)
+
+val token : Lexing.lexbuf -> Parsesmtlib.token
diff --git a/util/smtlib/lexsmtlib.mll b/util/smtlib/lexsmtlib.mll
new file mode 100644
index 00000000..e02e09df
--- /dev/null
+++ b/util/smtlib/lexsmtlib.mll
@@ -0,0 +1,48 @@
+{
+ (* auto-generated by gt *)
+
+open Parsesmtlib;;
+}
+
+rule token = parse
+| ['\t' ' ' ]+ { token lexbuf }
+| ';'  (_ # '\n')* { token lexbuf }
+| ['\n']+ as str { Smtlib_util.line := (!Smtlib_util.line + (String.length str)); token lexbuf }
+| "_" { UNDERSCORE }
+| "(" { LPAREN }
+| ")" { RPAREN }
+| "as" { AS }
+| "let" { LET }
+| "forall" { FORALL }
+| "exists" { EXISTS }
+| "!" { EXCLIMATIONPT }
+| "set-logic" { SETLOGIC }
+| "set-option" { SETOPTION }
+| "set-info" { SETINFO }
+| "declare-sort" { DECLARESORT }
+| "define-sort" { DEFINESORT }
+| "declare-fun" { DECLAREFUN }
+| "define-fun" { DEFINEFUN }
+| "push" { PUSH }
+| "pop" { POP }
+| "assert" { ASSERT }
+| "check-sat" { CHECKSAT }
+| "get-assertions" { GETASSERT }
+| "get-proof" { GETPROOF }
+| "get-unsat-core" { GETUNSATCORE }
+| "get-value" { GETVALUE }
+| "get-assignment" { GETASSIGN }
+| "get-option" { GETOPTION }
+| "get-info" { GETINFO }
+| "exit" { EXIT }
+|  '#' 'x' ['0'-'9' 'A'-'F' 'a'-'f']+  as str { HEXADECIMAL(str) }
+|  '#' 'b' ['0'-'1']+  as str { BINARY(str) }
+|  '|' ([ '!'-'~' ' ' '\n' '\t' '\r'] # ['\\' '|'])* '|'  as str { ASCIIWOR(str) }
+|  ':' ['a'-'z' 'A'-'Z' '0'-'9' '+' '-' '/' '*' '=' '%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@']+  as str { KEYWORD(str) }
+|  ['a'-'z' 'A'-'Z' '+' '-' '/' '*' '=''%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@'] ['a'-'z' 'A'-'Z' '0'-'9' '+' '-' '/' '*' '=''%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@']*  as str { SYMBOL(str) }
+|  '"' (([ '!'-'~' ' ' '\n' '\t' '\r' ] # ['\\' '"']) | ('\\' ['!'-'~' ' ' '\n' '\t' '\r'] ))* '"' as str { STRINGLIT(str) }
+|  ( '0' | ['1'-'9'] ['0'-'9']* )  as str { NUMERAL(str) }
+|  ( '0' | ['1'-'9'] ['0'-'9']* ) '.' ['0'-'9']+ as str { DECIMAL(str) }
+| eof { EOF }
+| _ {failwith((Lexing.lexeme lexbuf) ^
+": lexing error on line "^(string_of_int !Smtlib_util.line))}{}
diff --git a/util/smtlib/parsesmtlib.mly b/util/smtlib/parsesmtlib.mly
new file mode 100644
index 00000000..343ccb27
--- /dev/null
+++ b/util/smtlib/parsesmtlib.mly
@@ -0,0 +1,330 @@
+%{
+(* auto-generated by gt *)
+
+   open Smtlib_syntax;;
+let parse_error s =
+   print_string s;
+  print_string " on line ";
+  print_int !Smtlib_util.line;
+  print_string "\n";;
+
+%}
+
+%start main
+
+%token EOF AS ASSERT CHECKSAT DECLAREFUN DECLARESORT DEFINEFUN DEFINESORT EXCLIMATIONPT EXISTS EXIT FORALL GETASSERT GETASSIGN GETINFO GETOPTION GETPROOF GETUNSATCORE GETVALUE LET LPAREN POP PUSH RPAREN SETINFO SETLOGIC SETOPTION UNDERSCORE
+%token <string> ASCIIWOR BINARY DECIMAL HEXADECIMAL KEYWORD NUMERAL STRINGLIT SYMBOL
+
+%type <Smtlib_syntax.commands option> main
+
+%type <Smtlib_syntax.an_option> an_option
+
+%type <Smtlib_syntax.attribute> attribute
+
+%type <Smtlib_syntax.attributevalsexpr_attributevalue_sexpr5> attributevalsexpr_attributevalue_sexpr5
+
+%type <Smtlib_syntax.attributevalue> attributevalue
+
+%type <Smtlib_syntax.command> command
+
+%type <Smtlib_syntax.commanddeclarefun_command_sort13> commanddeclarefun_command_sort13
+
+%type <Smtlib_syntax.commanddefinefun_command_sortedvar15> commanddefinefun_command_sortedvar15
+
+%type <Smtlib_syntax.commanddefinesort_command_symbol11> commanddefinesort_command_symbol11
+
+%type <Smtlib_syntax.commandgetvalue_command_term24> commandgetvalue_command_term24
+
+%type <Smtlib_syntax.commands> commands
+
+%type <Smtlib_syntax.commands_commands_command30> commands_commands_command30
+
+%type <Smtlib_syntax.identifier> identifier
+
+%type <Smtlib_syntax.idunderscoresymnum_identifier_numeral33> idunderscoresymnum_identifier_numeral33
+
+%type <Smtlib_syntax.infoflag> infoflag
+
+%type <Smtlib_syntax.qualidentifier> qualidentifier
+
+%type <Smtlib_syntax.sexpr> sexpr
+
+%type <Smtlib_syntax.sexprinparen_sexpr_sexpr41> sexprinparen_sexpr_sexpr41
+
+%type <Smtlib_syntax.sort> sort
+
+%type <Smtlib_syntax.sortedvar> sortedvar
+
+%type <Smtlib_syntax.sortidsortmulti_sort_sort44> sortidsortmulti_sort_sort44
+
+%type <Smtlib_syntax.specconstant> specconstant
+
+%type <Smtlib_syntax.symbol> symbol
+
+%type <Smtlib_syntax.term> term
+
+%type <Smtlib_syntax.termexclimationpt_term_attribute64> termexclimationpt_term_attribute64
+
+%type <Smtlib_syntax.termexiststerm_term_sortedvar62> termexiststerm_term_sortedvar62
+
+%type <Smtlib_syntax.termforallterm_term_sortedvar60> termforallterm_term_sortedvar60
+
+%type <Smtlib_syntax.termletterm_term_varbinding58> termletterm_term_varbinding58
+
+%type <Smtlib_syntax.termqualidterm_term_term56> termqualidterm_term_term56
+
+%type <Smtlib_syntax.varbinding> varbinding
+
+%type <Smtlib_util.pd> cur_position
+
+%%
+
+main:
+| commands { Some($1) }
+| EOF { None }
+
+cur_position:
+| { Smtlib_util.cur_pd() }
+
+an_option:
+| attribute { AnOptionAttribute(pd_attribute $1, $1) }
+
+attribute:
+| cur_position KEYWORD { AttributeKeyword($1, $2) }
+
+attribute:
+| cur_position KEYWORD attributevalue { AttributeKeywordValue($1, $2, $3) }
+
+attributevalue:
+| specconstant { AttributeValSpecConst(pd_specconstant $1, $1) }
+
+attributevalue:
+| symbol { AttributeValSymbol(pd_symbol $1, $1) }
+
+attributevalue:
+| cur_position LPAREN attributevalsexpr_attributevalue_sexpr5 RPAREN { AttributeValSexpr($1, $3) }
+
+command:
+| cur_position LPAREN SETLOGIC symbol RPAREN { CommandSetLogic($1, $4) }
+
+command:
+| cur_position LPAREN SETOPTION an_option RPAREN { CommandSetOption($1, $4) }
+
+command:
+| cur_position LPAREN SETINFO attribute RPAREN { CommandSetInfo($1, $4) }
+
+command:
+| cur_position LPAREN DECLARESORT symbol NUMERAL RPAREN { CommandDeclareSort($1, $4, $5) }
+
+command:
+| cur_position LPAREN DEFINESORT symbol LPAREN commanddefinesort_command_symbol11 RPAREN sort RPAREN { CommandDefineSort($1, $4, $6, $8) }
+
+command:
+| cur_position LPAREN DECLAREFUN symbol LPAREN commanddeclarefun_command_sort13 RPAREN sort RPAREN { CommandDeclareFun($1, $4, $6, $8) }
+
+command:
+| cur_position LPAREN DEFINEFUN symbol LPAREN commanddefinefun_command_sortedvar15 RPAREN sort term RPAREN { CommandDefineFun($1, $4, $6, $8, $9) }
+
+command:
+| cur_position LPAREN PUSH NUMERAL RPAREN { CommandPush($1, $4) }
+
+command:
+| cur_position LPAREN POP NUMERAL RPAREN { CommandPop($1, $4) }
+
+command:
+| cur_position LPAREN ASSERT term RPAREN { CommandAssert($1, $4) }
+
+command:
+| cur_position LPAREN CHECKSAT RPAREN { CommandCheckSat($1) }
+
+command:
+| cur_position LPAREN GETASSERT RPAREN { CommandGetAssert($1) }
+
+command:
+| cur_position LPAREN GETPROOF RPAREN { CommandGetProof($1) }
+
+command:
+| cur_position LPAREN GETUNSATCORE RPAREN { CommandGetUnsatCore($1) }
+
+command:
+| cur_position LPAREN GETVALUE LPAREN commandgetvalue_command_term24 RPAREN RPAREN { CommandGetValue($1, $5) }
+
+command:
+| cur_position LPAREN GETASSIGN RPAREN { CommandGetAssign($1) }
+
+command:
+| cur_position LPAREN GETOPTION KEYWORD RPAREN { CommandGetOption($1, $4) }
+
+command:
+| cur_position LPAREN GETINFO infoflag RPAREN { CommandGetInfo($1, $4) }
+
+command:
+| cur_position LPAREN EXIT RPAREN { CommandExit($1) }
+
+commands:
+| commands_commands_command30 { Commands(pd_commands_commands_command30 $1, $1) }
+
+identifier:
+| symbol { IdSymbol(pd_symbol $1, $1) }
+
+identifier:
+| cur_position LPAREN UNDERSCORE symbol idunderscoresymnum_identifier_numeral33 RPAREN { IdUnderscoreSymNum($1, $4, $5) }
+
+infoflag:
+| cur_position KEYWORD { InfoFlagKeyword($1, $2) }
+
+qualidentifier:
+| identifier { QualIdentifierId(pd_identifier $1, $1) }
+
+qualidentifier:
+| cur_position LPAREN AS identifier sort RPAREN { QualIdentifierAs($1, $4, $5) }
+
+sexpr:
+| specconstant { SexprSpecConst(pd_specconstant $1, $1) }
+
+sexpr:
+| symbol { SexprSymbol(pd_symbol $1, $1) }
+
+sexpr:
+| cur_position KEYWORD { SexprKeyword($1, $2) }
+
+sexpr:
+| cur_position LPAREN sexprinparen_sexpr_sexpr41 RPAREN { SexprInParen($1, $3) }
+
+sort:
+| identifier { SortIdentifier(pd_identifier $1, $1) }
+
+sort:
+| cur_position LPAREN identifier sortidsortmulti_sort_sort44 RPAREN { SortIdSortMulti($1, $3, $4) }
+
+sortedvar:
+| cur_position LPAREN symbol sort RPAREN { SortedVarSymSort($1, $3, $4) }
+
+specconstant:
+| cur_position DECIMAL { SpecConstsDec($1, $2) }
+
+specconstant:
+| cur_position NUMERAL { SpecConstNum($1, $2) }
+
+specconstant:
+| cur_position STRINGLIT { SpecConstString($1, $2) }
+
+specconstant:
+| cur_position HEXADECIMAL { SpecConstsHex($1, $2) }
+
+specconstant:
+| cur_position BINARY { SpecConstsBinary($1, $2) }
+
+symbol:
+| cur_position SYMBOL { Symbol($1, $2) }
+
+symbol:
+| cur_position ASCIIWOR { SymbolWithOr($1, $2) }
+
+term:
+| specconstant { TermSpecConst(pd_specconstant $1, $1) }
+
+term:
+| qualidentifier { TermQualIdentifier(pd_qualidentifier $1, $1) }
+
+term:
+| cur_position LPAREN qualidentifier termqualidterm_term_term56 RPAREN { TermQualIdTerm($1, $3, $4) }
+
+term:
+| cur_position LPAREN LET LPAREN termletterm_term_varbinding58 RPAREN term RPAREN { TermLetTerm($1, $5, $7) }
+
+term:
+| cur_position LPAREN FORALL LPAREN termforallterm_term_sortedvar60 RPAREN term RPAREN { TermForAllTerm($1, $5, $7) }
+
+term:
+| cur_position LPAREN EXISTS LPAREN termexiststerm_term_sortedvar62 RPAREN term RPAREN { TermExistsTerm($1, $5, $7) }
+
+term:
+| cur_position LPAREN EXCLIMATIONPT term termexclimationpt_term_attribute64 RPAREN { TermExclimationPt($1, $4, $5) }
+
+varbinding:
+| cur_position LPAREN symbol term RPAREN { VarBindingSymTerm($1, $3, $4) }
+
+termexclimationpt_term_attribute64:
+| attribute { (pd_attribute $1, ($1)::[]) }
+
+termexclimationpt_term_attribute64:
+| attribute termexclimationpt_term_attribute64 { let (p, ( l1 )) = $2 in (pd_attribute $1, ($1)::(l1)) }
+
+termexiststerm_term_sortedvar62:
+| sortedvar { (pd_sortedvar $1, ($1)::[]) }
+
+termexiststerm_term_sortedvar62:
+| sortedvar termexiststerm_term_sortedvar62 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) }
+
+termforallterm_term_sortedvar60:
+| sortedvar { (pd_sortedvar $1, ($1)::[]) }
+
+termforallterm_term_sortedvar60:
+| sortedvar termforallterm_term_sortedvar60 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) }
+
+termletterm_term_varbinding58:
+| varbinding { (pd_varbinding $1, ($1)::[]) }
+
+termletterm_term_varbinding58:
+| varbinding termletterm_term_varbinding58 { let (p, ( l1 )) = $2 in (pd_varbinding $1, ($1)::(l1)) }
+
+termqualidterm_term_term56:
+| term { (pd_term $1, ($1)::[]) }
+
+termqualidterm_term_term56:
+| term termqualidterm_term_term56 { let (p, ( l1 )) = $2 in (pd_term $1, ($1)::(l1)) }
+
+sortidsortmulti_sort_sort44:
+| sort { (pd_sort $1, ($1)::[]) }
+
+sortidsortmulti_sort_sort44:
+| sort sortidsortmulti_sort_sort44 { let (p, ( l1 )) = $2 in (pd_sort $1, ($1)::(l1)) }
+
+sexprinparen_sexpr_sexpr41:
+| cur_position { ($1, []) }
+
+sexprinparen_sexpr_sexpr41:
+| sexpr sexprinparen_sexpr_sexpr41 { let (p, ( l1 )) = $2 in (pd_sexpr $1, ($1)::(l1)) }
+
+idunderscoresymnum_identifier_numeral33:
+| cur_position NUMERAL { ($1, ($2)::[]) }
+
+idunderscoresymnum_identifier_numeral33:
+| cur_position NUMERAL idunderscoresymnum_identifier_numeral33 { let (p, ( l1 )) = $3 in ($1, ($2)::(l1)) }
+
+commands_commands_command30:
+| cur_position { ($1, []) }
+
+commands_commands_command30:
+| command commands_commands_command30 { let (p, ( l1 )) = $2 in (pd_command $1, ($1)::(l1)) }
+
+commandgetvalue_command_term24:
+| term { (pd_term $1, ($1)::[]) }
+
+commandgetvalue_command_term24:
+| term commandgetvalue_command_term24 { let (p, ( l1 )) = $2 in (pd_term $1, ($1)::(l1)) }
+
+commanddefinefun_command_sortedvar15:
+| cur_position { ($1, []) }
+
+commanddefinefun_command_sortedvar15:
+| sortedvar commanddefinefun_command_sortedvar15 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) }
+
+commanddeclarefun_command_sort13:
+| cur_position { ($1, []) }
+
+commanddeclarefun_command_sort13:
+| sort commanddeclarefun_command_sort13 { let (p, ( l1 )) = $2 in (pd_sort $1, ($1)::(l1)) }
+
+commanddefinesort_command_symbol11:
+| cur_position { ($1, []) }
+
+commanddefinesort_command_symbol11:
+| symbol commanddefinesort_command_symbol11 { let (p, ( l1 )) = $2 in (pd_symbol $1, ($1)::(l1)) }
+
+attributevalsexpr_attributevalue_sexpr5:
+| cur_position { ($1, []) }
+
+attributevalsexpr_attributevalue_sexpr5:
+| sexpr attributevalsexpr_attributevalue_sexpr5 { let (p, ( l1 )) = $2 in (pd_sexpr $1, ($1)::(l1)) }
diff --git a/util/smtlib/smtlib.ml b/util/smtlib/smtlib.ml
new file mode 100644
index 00000000..377eefb4
--- /dev/null
+++ b/util/smtlib/smtlib.ml
@@ -0,0 +1,103 @@
+(* Copyright 2014 INRIA **)
+
+open Smtlib_syntax
+
+module F = Sat.Fsat
+module T = Sat.Tseitin
+
+exception Bad_arity of string
+exception Unknown_command
+exception Incomplete_translation
+
+(* Environment *)
+let env : (string, T.t) Hashtbl.t = Hashtbl.create 57;;
+Hashtbl.add env "true" T.f_true;;
+Hashtbl.add env "false" T.f_false;;
+
+let get_var =
+    fun s ->
+        try
+            Hashtbl.find env s
+        with Not_found ->
+            let f = T.make_atom (F.fresh ()) in
+            Hashtbl.add env s f;
+            f
+
+(* Term translation *)
+let translate_const = function
+    | SpecConstsDec(_, s)
+    | SpecConstNum(_, s)
+    | SpecConstString(_, s)
+    | SpecConstsHex(_, s)
+    | SpecConstsBinary(_, s) -> get_var s
+
+let translate_symbol = function
+    | Symbol(_, s)
+    | SymbolWithOr(_, s) -> s
+
+let translate_id = function
+    | IdSymbol(_, s) -> translate_symbol s
+    | IdUnderscoreSymNum(_, s, n) -> raise Incomplete_translation
+
+let translate_sort = function
+    | SortIdentifier(_, id) ->
+            let s = translate_id id in
+            if s <> "Bool" then raise Incomplete_translation
+    | _ -> raise Incomplete_translation
+
+let translate_qualid = function
+    | QualIdentifierId(_, id) -> translate_id id
+    | QualIdentifierAs(_, id, s) -> raise Incomplete_translation
+
+let left_assoc s f = function
+    | x :: r -> List.fold_left f x r
+    | _ -> raise (Bad_arity s)
+
+let right_assoc s f = function
+    | x :: r -> List.fold_right f r x
+    | _ -> raise (Bad_arity s)
+
+let rec translate_term = function
+    | TermSpecConst(_, const) -> translate_const const
+    | TermQualIdentifier(_, id) -> get_var (translate_qualid id)
+    | TermQualIdTerm(_, f, (_, l)) ->
+            begin match (translate_qualid f), (List.map translate_term l) with
+            (* CORE theory translation - '=', 'distinct','ite' not yet implemented *)
+            | "not", [e] -> T.make_not e
+            | "not", _ -> raise (Bad_arity "not")
+            | "and" as s, l -> T.make_and l
+            | "or" as s, l -> T.make_or l
+            | "xor" as s, l -> left_assoc s T.make_xor l
+            | "=>" as s, l -> right_assoc s T.make_imply l
+            | _ -> raise Unknown_command
+            end
+    | _ -> raise Incomplete_translation
+
+(* Command Translation *)
+let translate_command = function
+    | CommandDeclareFun(_, s, (_, []), ret) ->
+            ignore (translate_sort ret);
+            ignore (get_var (translate_symbol s));
+            None
+    | CommandAssert(_, t) ->
+            Some (translate_term t)
+    | _ -> None
+
+let rec translate_command_list acc = function
+    | [] -> acc
+    | c :: r ->
+                begin match translate_command c with
+                | None -> translate_command_list acc r
+                | Some t -> translate_command_list (t :: acc) r
+                end
+
+let translate = function
+    | Some Commands (_, (_, l)) -> List.rev (translate_command_list [] l)
+    | None -> []
+
+let parse file =
+    let f = open_in file in
+    let lexbuf = Lexing.from_channel f in
+    let commands = Parsesmtlib.main Lexsmtlib.token lexbuf in
+    close_in f;
+    translate commands
diff --git a/util/smtlib/smtlib.mli b/util/smtlib/smtlib.mli
new file mode 100644
index 00000000..19ff02bc
--- /dev/null
+++ b/util/smtlib/smtlib.mli
@@ -0,0 +1,3 @@
+(* Copyright 2014 INRIA *)
+
+val parse : string -> Sat.Tseitin.t list
diff --git a/util/smtlib/smtlib_syntax.ml b/util/smtlib/smtlib_syntax.ml
new file mode 100644
index 00000000..c3cac59a
--- /dev/null
+++ b/util/smtlib/smtlib_syntax.ml
@@ -0,0 +1,229 @@
+(* auto-generated by gt *)
+
+open Smtlib_util;;
+
+type dummy = Dummy 
+and an_option = | AnOptionAttribute of pd * attribute
+and attribute = | AttributeKeyword of pd * string | AttributeKeywordValue of pd * string * attributevalue
+and attributevalue = | AttributeValSpecConst of pd * specconstant | AttributeValSymbol of pd * symbol | AttributeValSexpr of pd * attributevalsexpr_attributevalue_sexpr5
+and command = | CommandSetLogic of pd * symbol | CommandSetOption of pd * an_option | CommandSetInfo of pd * attribute | CommandDeclareSort of pd * symbol * string | CommandDefineSort of pd * symbol * commanddefinesort_command_symbol11 * sort | CommandDeclareFun of pd * symbol * commanddeclarefun_command_sort13 * sort | CommandDefineFun of pd * symbol * commanddefinefun_command_sortedvar15 * sort * term | CommandPush of pd * string | CommandPop of pd * string | CommandAssert of pd * term | CommandCheckSat of pd | CommandGetAssert of pd | CommandGetProof of pd | CommandGetUnsatCore of pd | CommandGetValue of pd * commandgetvalue_command_term24 | CommandGetAssign of pd | CommandGetOption of pd * string | CommandGetInfo of pd * infoflag | CommandExit of pd
+and commands = | Commands of pd * commands_commands_command30
+and identifier = | IdSymbol of pd * symbol | IdUnderscoreSymNum of pd * symbol * idunderscoresymnum_identifier_numeral33
+and infoflag = | InfoFlagKeyword of pd * string
+and qualidentifier = | QualIdentifierId of pd * identifier | QualIdentifierAs of pd * identifier * sort
+and sexpr = | SexprSpecConst of pd * specconstant | SexprSymbol of pd * symbol | SexprKeyword of pd * string | SexprInParen of pd * sexprinparen_sexpr_sexpr41
+and sort = | SortIdentifier of pd * identifier | SortIdSortMulti of pd * identifier * sortidsortmulti_sort_sort44
+and sortedvar = | SortedVarSymSort of pd * symbol * sort
+and specconstant = | SpecConstsDec of pd * string | SpecConstNum of pd * string | SpecConstString of pd * string | SpecConstsHex of pd * string | SpecConstsBinary of pd * string
+and symbol = | Symbol of pd * string | SymbolWithOr of pd * string
+and term = | TermSpecConst of pd * specconstant | TermQualIdentifier of pd * qualidentifier | TermQualIdTerm of pd * qualidentifier * termqualidterm_term_term56 | TermLetTerm of pd * termletterm_term_varbinding58 * term | TermForAllTerm of pd * termforallterm_term_sortedvar60 * term | TermExistsTerm of pd * termexiststerm_term_sortedvar62 * term | TermExclimationPt of pd * term * termexclimationpt_term_attribute64
+and varbinding = | VarBindingSymTerm of pd * symbol * term
+and termexclimationpt_term_attribute64 = pd * ( attribute) list
+and termexiststerm_term_sortedvar62 = pd * ( sortedvar) list
+and termforallterm_term_sortedvar60 = pd * ( sortedvar) list
+and termletterm_term_varbinding58 = pd * ( varbinding) list
+and termqualidterm_term_term56 = pd * ( term) list
+and sortidsortmulti_sort_sort44 = pd * ( sort) list
+and sexprinparen_sexpr_sexpr41 = pd * ( sexpr) list
+and idunderscoresymnum_identifier_numeral33 = pd * ( string) list
+and commands_commands_command30 = pd * ( command) list
+and commandgetvalue_command_term24 = pd * ( term) list
+and commanddefinefun_command_sortedvar15 = pd * ( sortedvar) list
+and commanddeclarefun_command_sort13 = pd * ( sort) list
+and commanddefinesort_command_symbol11 = pd * ( symbol) list
+and attributevalsexpr_attributevalue_sexpr5 = pd * ( sexpr) list;;
+
+(* pd stands for pos (position) and extradata *)
+let rec dummy () = () 
+and pd_an_option = function 
+  | AnOptionAttribute(d,_) -> d
+
+and pd_attribute = function 
+  | AttributeKeyword(d,_) -> d
+
+  | AttributeKeywordValue(d,_,_) -> d
+
+and pd_attributevalue = function 
+  | AttributeValSpecConst(d,_) -> d
+
+  | AttributeValSymbol(d,_) -> d
+
+  | AttributeValSexpr(d,_) -> d
+
+and pd_command = function 
+  | CommandSetLogic(d,_) -> d
+
+  | CommandSetOption(d,_) -> d
+
+  | CommandSetInfo(d,_) -> d
+
+  | CommandDeclareSort(d,_,_) -> d
+
+  | CommandDefineSort(d,_,_,_) -> d
+
+  | CommandDeclareFun(d,_,_,_) -> d
+
+  | CommandDefineFun(d,_,_,_,_) -> d
+
+  | CommandPush(d,_) -> d
+
+  | CommandPop(d,_) -> d
+
+  | CommandAssert(d,_) -> d
+
+  | CommandCheckSat(d) -> d
+
+  | CommandGetAssert(d) -> d
+
+  | CommandGetProof(d) -> d
+
+  | CommandGetUnsatCore(d) -> d
+
+  | CommandGetValue(d,_) -> d
+
+  | CommandGetAssign(d) -> d
+
+  | CommandGetOption(d,_) -> d
+
+  | CommandGetInfo(d,_) -> d
+
+  | CommandExit(d) -> d
+
+and pd_commands = function 
+  | Commands(d,_) -> d
+
+and pd_identifier = function 
+  | IdSymbol(d,_) -> d
+
+  | IdUnderscoreSymNum(d,_,_) -> d
+
+and pd_infoflag = function 
+  | InfoFlagKeyword(d,_) -> d
+
+and pd_qualidentifier = function 
+  | QualIdentifierId(d,_) -> d
+
+  | QualIdentifierAs(d,_,_) -> d
+
+and pd_sexpr = function 
+  | SexprSpecConst(d,_) -> d
+
+  | SexprSymbol(d,_) -> d
+
+  | SexprKeyword(d,_) -> d
+
+  | SexprInParen(d,_) -> d
+
+and pd_sort = function 
+  | SortIdentifier(d,_) -> d
+
+  | SortIdSortMulti(d,_,_) -> d
+
+and pd_sortedvar = function 
+  | SortedVarSymSort(d,_,_) -> d
+
+and pd_specconstant = function 
+  | SpecConstsDec(d,_) -> d
+
+  | SpecConstNum(d,_) -> d
+
+  | SpecConstString(d,_) -> d
+
+  | SpecConstsHex(d,_) -> d
+
+  | SpecConstsBinary(d,_) -> d
+
+and pd_symbol = function 
+  | Symbol(d,_) -> d
+
+  | SymbolWithOr(d,_) -> d
+
+and pd_term = function 
+  | TermSpecConst(d,_) -> d
+
+  | TermQualIdentifier(d,_) -> d
+
+  | TermQualIdTerm(d,_,_) -> d
+
+  | TermLetTerm(d,_,_) -> d
+
+  | TermForAllTerm(d,_,_) -> d
+
+  | TermExistsTerm(d,_,_) -> d
+
+  | TermExclimationPt(d,_,_) -> d
+
+and pd_varbinding = function 
+  | VarBindingSymTerm(d,_,_) -> d
+
+and pd_termexclimationpt_term_attribute64 = function 
+  | (d,[]) -> d
+
+  | (d,( _ )::f1239o2) -> d
+
+and pd_termexiststerm_term_sortedvar62 = function 
+  | (d,[]) -> d
+
+  | (d,( _ )::f1239o2) -> d
+
+and pd_termforallterm_term_sortedvar60 = function 
+  | (d,[]) -> d
+
+  | (d,( _ )::f1239o2) -> d
+
+and pd_termletterm_term_varbinding58 = function 
+  | (d,[]) -> d
+
+  | (d,( _ )::f1239o2) -> d
+
+and pd_termqualidterm_term_term56 = function 
+  | (d,[]) -> d
+
+  | (d,( _ )::f1239o2) -> d
+
+and pd_sortidsortmulti_sort_sort44 = function 
+  | (d,[]) -> d
+
+  | (d,( _ )::f1239o2) -> d
+
+and pd_sexprinparen_sexpr_sexpr41 = function 
+  | (d,[]) -> d
+
+  | (d,( _ )::f1239o2) -> d
+
+and pd_idunderscoresymnum_identifier_numeral33 = function 
+  | (d,[]) -> d
+
+  | (d,( _ )::f1239o2) -> d
+
+and pd_commands_commands_command30 = function 
+  | (d,[]) -> d
+
+  | (d,( _ )::f1239o2) -> d
+
+and pd_commandgetvalue_command_term24 = function 
+  | (d,[]) -> d
+
+  | (d,( _ )::f1239o2) -> d
+
+and pd_commanddefinefun_command_sortedvar15 = function 
+  | (d,[]) -> d
+
+  | (d,( _ )::f1239o2) -> d
+
+and pd_commanddeclarefun_command_sort13 = function 
+  | (d,[]) -> d
+
+  | (d,( _ )::f1239o2) -> d
+
+and pd_commanddefinesort_command_symbol11 = function 
+  | (d,[]) -> d
+
+  | (d,( _ )::f1239o2) -> d
+
+and pd_attributevalsexpr_attributevalue_sexpr5 = function 
+  | (d,[]) -> d
+
+  | (d,( _ )::f1239o2) -> d
+;;
+let pd e = pd_commands e;;
\ No newline at end of file
diff --git a/util/smtlib/smtlib_syntax.mli b/util/smtlib/smtlib_syntax.mli
new file mode 100644
index 00000000..f4c0223d
--- /dev/null
+++ b/util/smtlib/smtlib_syntax.mli
@@ -0,0 +1,119 @@
+(* Copyright 2014 INRIA *)
+
+type dummy = Dummy
+and an_option = AnOptionAttribute of Smtlib_util.pd * attribute
+and attribute =
+    AttributeKeyword of Smtlib_util.pd * string
+  | AttributeKeywordValue of Smtlib_util.pd * string * attributevalue
+and attributevalue =
+    AttributeValSpecConst of Smtlib_util.pd * specconstant
+  | AttributeValSymbol of Smtlib_util.pd * symbol
+  | AttributeValSexpr of Smtlib_util.pd *
+      attributevalsexpr_attributevalue_sexpr5
+and command =
+    CommandSetLogic of Smtlib_util.pd * symbol
+  | CommandSetOption of Smtlib_util.pd * an_option
+  | CommandSetInfo of Smtlib_util.pd * attribute
+  | CommandDeclareSort of Smtlib_util.pd * symbol * string
+  | CommandDefineSort of Smtlib_util.pd * symbol *
+      commanddefinesort_command_symbol11 * sort
+  | CommandDeclareFun of Smtlib_util.pd * symbol *
+      commanddeclarefun_command_sort13 * sort
+  | CommandDefineFun of Smtlib_util.pd * symbol *
+      commanddefinefun_command_sortedvar15 * sort * term
+  | CommandPush of Smtlib_util.pd * string
+  | CommandPop of Smtlib_util.pd * string
+  | CommandAssert of Smtlib_util.pd * term
+  | CommandCheckSat of Smtlib_util.pd
+  | CommandGetAssert of Smtlib_util.pd
+  | CommandGetProof of Smtlib_util.pd
+  | CommandGetUnsatCore of Smtlib_util.pd
+  | CommandGetValue of Smtlib_util.pd * commandgetvalue_command_term24
+  | CommandGetAssign of Smtlib_util.pd
+  | CommandGetOption of Smtlib_util.pd * string
+  | CommandGetInfo of Smtlib_util.pd * infoflag
+  | CommandExit of Smtlib_util.pd
+and commands = Commands of Smtlib_util.pd * commands_commands_command30
+and identifier =
+    IdSymbol of Smtlib_util.pd * symbol
+  | IdUnderscoreSymNum of Smtlib_util.pd * symbol *
+      idunderscoresymnum_identifier_numeral33
+and infoflag = InfoFlagKeyword of Smtlib_util.pd * string
+and qualidentifier =
+    QualIdentifierId of Smtlib_util.pd * identifier
+  | QualIdentifierAs of Smtlib_util.pd * identifier * sort
+and sexpr =
+    SexprSpecConst of Smtlib_util.pd * specconstant
+  | SexprSymbol of Smtlib_util.pd * symbol
+  | SexprKeyword of Smtlib_util.pd * string
+  | SexprInParen of Smtlib_util.pd * sexprinparen_sexpr_sexpr41
+and sort =
+    SortIdentifier of Smtlib_util.pd * identifier
+  | SortIdSortMulti of Smtlib_util.pd * identifier *
+      sortidsortmulti_sort_sort44
+and sortedvar = SortedVarSymSort of Smtlib_util.pd * symbol * sort
+and specconstant =
+    SpecConstsDec of Smtlib_util.pd * string
+  | SpecConstNum of Smtlib_util.pd * string
+  | SpecConstString of Smtlib_util.pd * string
+  | SpecConstsHex of Smtlib_util.pd * string
+  | SpecConstsBinary of Smtlib_util.pd * string
+and symbol =
+    Symbol of Smtlib_util.pd * string
+  | SymbolWithOr of Smtlib_util.pd * string
+and term =
+    TermSpecConst of Smtlib_util.pd * specconstant
+  | TermQualIdentifier of Smtlib_util.pd * qualidentifier
+  | TermQualIdTerm of Smtlib_util.pd * qualidentifier *
+      termqualidterm_term_term56
+  | TermLetTerm of Smtlib_util.pd * termletterm_term_varbinding58 * term
+  | TermForAllTerm of Smtlib_util.pd * termforallterm_term_sortedvar60 * term
+  | TermExistsTerm of Smtlib_util.pd * termexiststerm_term_sortedvar62 * term
+  | TermExclimationPt of Smtlib_util.pd * term *
+      termexclimationpt_term_attribute64
+and varbinding = VarBindingSymTerm of Smtlib_util.pd * symbol * term
+and termexclimationpt_term_attribute64 = Smtlib_util.pd * attribute list
+and termexiststerm_term_sortedvar62 = Smtlib_util.pd * sortedvar list
+and termforallterm_term_sortedvar60 = Smtlib_util.pd * sortedvar list
+and termletterm_term_varbinding58 = Smtlib_util.pd * varbinding list
+and termqualidterm_term_term56 = Smtlib_util.pd * term list
+and sortidsortmulti_sort_sort44 = Smtlib_util.pd * sort list
+and sexprinparen_sexpr_sexpr41 = Smtlib_util.pd * sexpr list
+and idunderscoresymnum_identifier_numeral33 = Smtlib_util.pd * string list
+and commands_commands_command30 = Smtlib_util.pd * command list
+and commandgetvalue_command_term24 = Smtlib_util.pd * term list
+and commanddefinefun_command_sortedvar15 = Smtlib_util.pd * sortedvar list
+and commanddeclarefun_command_sort13 = Smtlib_util.pd * sort list
+and commanddefinesort_command_symbol11 = Smtlib_util.pd * symbol list
+and attributevalsexpr_attributevalue_sexpr5 = Smtlib_util.pd * sexpr list
+val dummy : unit -> unit
+val pd_an_option : an_option -> Smtlib_util.pd
+val pd_attribute : attribute -> Smtlib_util.pd
+val pd_attributevalue : attributevalue -> Smtlib_util.pd
+val pd_command : command -> Smtlib_util.pd
+val pd_commands : commands -> Smtlib_util.pd
+val pd_identifier : identifier -> Smtlib_util.pd
+val pd_infoflag : infoflag -> Smtlib_util.pd
+val pd_qualidentifier : qualidentifier -> Smtlib_util.pd
+val pd_sexpr : sexpr -> Smtlib_util.pd
+val pd_sort : sort -> Smtlib_util.pd
+val pd_sortedvar : sortedvar -> Smtlib_util.pd
+val pd_specconstant : specconstant -> Smtlib_util.pd
+val pd_symbol : symbol -> Smtlib_util.pd
+val pd_term : term -> Smtlib_util.pd
+val pd_varbinding : varbinding -> Smtlib_util.pd
+val pd_termexclimationpt_term_attribute64 : 'a * 'b list -> 'a
+val pd_termexiststerm_term_sortedvar62 : 'a * 'b list -> 'a
+val pd_termforallterm_term_sortedvar60 : 'a * 'b list -> 'a
+val pd_termletterm_term_varbinding58 : 'a * 'b list -> 'a
+val pd_termqualidterm_term_term56 : 'a * 'b list -> 'a
+val pd_sortidsortmulti_sort_sort44 : 'a * 'b list -> 'a
+val pd_sexprinparen_sexpr_sexpr41 : 'a * 'b list -> 'a
+val pd_idunderscoresymnum_identifier_numeral33 : 'a * 'b list -> 'a
+val pd_commands_commands_command30 : 'a * 'b list -> 'a
+val pd_commandgetvalue_command_term24 : 'a * 'b list -> 'a
+val pd_commanddefinefun_command_sortedvar15 : 'a * 'b list -> 'a
+val pd_commanddeclarefun_command_sort13 : 'a * 'b list -> 'a
+val pd_commanddefinesort_command_symbol11 : 'a * 'b list -> 'a
+val pd_attributevalsexpr_attributevalue_sexpr5 : 'a * 'b list -> 'a
+val pd : commands -> Smtlib_util.pd
diff --git a/util/smtlib/smtlib_util.ml b/util/smtlib/smtlib_util.ml
new file mode 100644
index 00000000..8e1da4d5
--- /dev/null
+++ b/util/smtlib/smtlib_util.ml
@@ -0,0 +1,12 @@
+(* auto-generated by gt *)
+
+(* no extra data from grammar file. *)
+type extradata = unit;;
+let initial_data() = ();;
+
+let file = ref "stdin";;
+let line = ref 1;;
+type pos = int;;
+let string_of_pos p = "line "^(string_of_int p);;
+let cur_pd() = (!line, initial_data());;   (* "pd": pos + extradata *) 
+type pd = pos * extradata;;
diff --git a/util/smtlib/smtlib_util.mli b/util/smtlib/smtlib_util.mli
new file mode 100644
index 00000000..8afbce37
--- /dev/null
+++ b/util/smtlib/smtlib_util.mli
@@ -0,0 +1,8 @@
+type extradata = unit
+val initial_data : unit -> unit
+val file : string ref
+val line : int ref
+type pos = int
+val string_of_pos : int -> string
+val cur_pd : unit -> int * unit
+type pd = pos * extradata