diff --git a/TODO.md b/TODO.md
index 019ddf7e..e070e88a 100644
--- a/TODO.md
+++ b/TODO.md
@@ -2,12 +2,16 @@
 
 ## Main goals
 
+- Add a backend to send proofs to dedukti
+    * First, pure resolution proofs
+    * Then, require theories to output lemma proofs for dedukti (in some format yet to be decided)
 - Allow to plug one's code into boolean propagation
     * react upon propagation (possibly by propagating more, or side-effect)
     * more advanced/specific propagation (2-clauses)?
     * implement 'constraints' (see https://www.lri.fr/~conchon/TER/2013/3/minisat.pdf )
-- Adapt old code for theories, inorder to plug it into new Solver Functor
+- Adapt old code for theories, in order to plug it into new Solver Functor
 
 ## Long term goals
 
 - max-sat/max-smt
+- coq proofs ?
diff --git a/util/sat_solve.ml b/util/sat_solve.ml
index b9dfe668..3b9dee35 100644
--- a/util/sat_solve.ml
+++ b/util/sat_solve.ml
@@ -213,7 +213,7 @@ let () =
   with
   | Incorrect_model ->
     print "Internal error : incorrect *sat* model";
-    exit 2
+    exit 4
   | Out_of_time ->
     print "Time limit exceeded";
     exit 2