diff --git a/src/backend/Dimacs.ml b/src/backend/Dimacs.ml
deleted file mode 100644
index cb17851d..00000000
--- a/src/backend/Dimacs.ml
+++ /dev/null
@@ -1,138 +0,0 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
-Copyright 2014 Simon Cruanes
-*)
-
-open Msat
-
-module type ARG = sig
-  type clause
-  val lits : clause -> int list
-end
-
-module type S = sig
-  type st
-
-  type clause
-  (** The type of clauses *)
-
-  val export :
-    st ->
-    Format.formatter ->
-    hyps:clause Vec.t ->
-    history:clause Vec.t ->
-    local:clause Vec.t ->
-    unit
-
-  val export_icnf :
-    Format.formatter ->
-    hyps:clause Vec.t ->
-    history:clause Vec.t ->
-    local:clause Vec.t ->
-    unit
-
-end
-
-module Make(St : Msat.S)(A: ARG with type clause = St.clause) = struct
-  type st = St.t
-
-  let pp_dimacs fmt c =
-    let lits = A.lits c in
-    List.iter (fun p -> Format.fprintf fmt "%d " p) lits;
-    Format.fprintf fmt "0"
-
-
-  (* Dimacs & iCNF export *)
-  let export_vec name fmt vec =
-    Format.fprintf fmt "c %s@,%a@," name (Vec.pp ~sep:"" pp_dimacs) vec
-
-  let export_assumption fmt vec =
-    Format.fprintf fmt "c Local assumptions@,a %a@," pp_dimacs vec
-
-  let export_icnf_aux r name map_filter fmt vec =
-    let aux fmt _ =
-      for i = !r to (Vec.size vec) - 1 do
-        let x = Vec.get vec i in
-        match map_filter x with
-        | None -> ()
-        | Some _ -> Format.fprintf fmt "%a@," pp_dimacs (Vec.get vec i)
-      done;
-      r := Vec.size vec
-    in
-    Format.fprintf fmt "c %s@,%a" name aux vec
-
-  (* TODO
-  let map_filter_learnt c =
-    match P.Clause.premise c with
-    | St.Hyp | St.Local -> assert false
-    | St.Lemma _ -> Some c
-    | St.History l ->
-      begin match l with
-        | [] -> assert false
-        | d :: _ ->
-          begin match St.Clause.premise d with
-            | St.Lemma _ -> Some d
-            | St.Hyp | St.Local | St.History _ -> None
-          end
-      end
-
-  let filter_vec learnt =
-    let lemmas = Vec.create() in
-    Vec.iter (fun c ->
-        match map_filter_learnt c with
-        | None -> ()
-        | Some d -> Vec.push lemmas d
-      ) learnt;
-    lemmas
-     *)
-
-  let export st fmt ~hyps ~history ~local =
-    assert false
-    (* FIXME
-    assert (Vec.for_all (fun c -> St.Clause.premise c = St.Hyp) hyps);
-    (* Learnt clauses, then filtered to only keep only
-       the theory lemmas; all other learnt clauses should be logical
-       consequences of the rest. *)
-    let lemmas = filter_vec history in
-    let lemmas = history in
-    (* Local assertions *)
-    assert (Vec.for_all (fun c -> St.Local = St.Clause.premise c) local);
-    (* Number of atoms and clauses *)
-    let n = St.nb_elt st in
-    let m = Vec.size local + Vec.size hyps + Vec.size lemmas in
-    Format.fprintf fmt
-      "@[<v>p cnf %d %d@,%a%a%a@]@." n m
-      (export_vec "Local assumptions") local
-      (export_vec "Hypotheses") hyps
-      (export_vec "Lemmas") lemmas
-       *)
-
-  (* Refs to remember what portion of a problem has been printed *)
-  let icnf_hyp = ref 0
-  let icnf_lemmas = ref 0
-
-  let export_icnf fmt ~hyps ~history ~local =
-    assert false
-    (* FIXME
-    assert (Vec.for_all (fun c -> St.Clause.premise c = St.Hyp) hyps);
-    let lemmas = history in
-    (* Local assertions *)
-    let l = List.map
-        (fun c -> match St.Clause.premise c, St.Clause.atoms c with
-             | St.Local, [| a |] -> a
-             | _ -> assert false)
-        (Vec.to_list local)
-    in
-    let local = St.Clause.make l St.Local in
-    (* Number of atoms and clauses *)
-    Format.fprintf fmt
-      "@[<v>%s@,%a%a%a@]@."
-      (if !icnf_hyp = 0 && !icnf_lemmas = 0 then "p inccnf" else "")
-      (export_icnf_aux icnf_hyp "Hypotheses" (fun x -> Some x)) hyps
-      (export_icnf_aux icnf_lemmas "Lemmas" map_filter_learnt) lemmas
-      export_assumption local
-       *)
-
-end
-
diff --git a/src/backend/Dimacs.mli b/src/backend/Dimacs.mli
deleted file mode 100644
index aada5010..00000000
--- a/src/backend/Dimacs.mli
+++ /dev/null
@@ -1,55 +0,0 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
-Copyright 2014 Simon Cruanes
-*)
-
-(** Dimacs backend for problems
-
-    This module provides functiosn to export problems to the dimacs and
-    iCNF formats.
-*)
-
-open Msat
-
-module type ARG = sig
-  type clause
-  val lits : clause -> int list
-end
-
-module type S = sig
-  type st
-
-  type clause
-  (** The type of clauses *)
-
-  val export :
-    st ->
-    Format.formatter ->
-    hyps:clause Vec.t ->
-    history:clause Vec.t ->
-    local:clause Vec.t ->
-    unit
-  (** Export the given clause vectors to the dimacs format.
-      The arguments should be transmitted directly from the corresponding
-      function of the {Internal} module. *)
-
-  val export_icnf :
-    Format.formatter ->
-    hyps:clause Vec.t ->
-    history:clause Vec.t ->
-    local:clause Vec.t ->
-    unit
-  (** Export the given clause vectors to the dimacs format.
-      The arguments should be transmitted directly from the corresponding
-      function of the {Internal} module.
-      This function may be called multiple times in order to add
-      new clauses (and new local hyps) to the problem.
-  *)
-
-end
-
-module Make(St: Msat.S)(A: ARG with type clause = St.clause)
-  : S with type clause := St.clause and type st = St.t
-(** Functor to create a module for exporting probems to the dimacs (& iCNF) formats. *)
-