diff --git a/.gitignore b/.gitignore
index cb485aab..75bc3997 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,4 @@
 _build/
-tests/main
 *.annot
 *.native
 *.log
@@ -8,3 +7,4 @@ tests/main
 .session
 *.docdir
 util/log.ml
+msat
diff --git a/Makefile b/Makefile
index 8f9cdbab..cd275265 100644
--- a/Makefile
+++ b/Makefile
@@ -6,8 +6,7 @@ FLAGS=
 #-ocamlc ocamlopt -cflag -O3
 DIRS=-Is solver,sat,smt,backend,util,util/smtlib
 DOC=msat.docdir/index.html
-TEST=sat_solve.native
-
+BIN=main.native
 NAME=msat
 
 LIB=$(addprefix $(NAME), .cma .cmxa .cmxs)
@@ -20,10 +19,11 @@ lib:
 doc:
 	$(COMP) $(FLAGS) $(DIRS) $(DOC)
 
-build-test:
-	$(COMP) $(FLAGS) $(DIRS) $(TEST)
+bin:
+	$(COMP) $(FLAGS) $(DIRS) $(BIN)
+	cp $(BIN) $(NAME) && rm $(BIN)
 
-test: build-test
+test: bin
 	@/usr/bin/time -f "%e" ./tests/run smt
 	@/usr/bin/time -f "%e" ./tests/run mcsat
 
@@ -33,12 +33,6 @@ enable_log:
 disable_log:
 	cd util; ln -sf log_dummy.ml log.ml
 
-bench: build-test
-	cd bench && $(MAKE)
-
-stats:
-	@./bench_stats.native
-
 log:
 	cat _build/$(LOG) || true
 
@@ -57,4 +51,4 @@ reinstall: all
 	ocamlfind remove msat || true
 	ocamlfind install msat $(TO_INSTALL)
 
-.PHONY: clean doc all bench install uninstall reinstall enable_log disable_log
+.PHONY: clean doc all bench install uninstall reinstall enable_log disable_log bin test
diff --git a/bench/Makefile b/bench/Makefile
deleted file mode 100644
index 485c1985..00000000
--- a/bench/Makefile
+++ /dev/null
@@ -1,36 +0,0 @@
-SOLVER 	:=../sat_solve.native
-OPTIONS :=-time 30s -size 1G
-
-LOGDIR 	:= $(shell echo "./logs/`git rev-parse HEAD`")
-INDEX	:= $(shell echo "./$(LOGDIR)/index")
-CNF 	:= $(shell find -L ./ -name "*.cnf" -type f)
-DONE 	:= $(addprefix $(LOGDIR)/raw/, $(CNF:=.done))
-
-PROVER := $(shell echo "./$(LOGDIR)/prover")
-CMD    := $(PROVER) $(OPTIONS)
-
-DATE    = date +'%H:%M:%S %d/%m/%Y'
-
-all: $(INDEX)
-
-sync:
-	rsync -avz rsync://gbury.eu/benchs/ ./
-
-$(INDEX): dummy $(PROVER) $(DONE)
-	@echo "Bench ended for commit `git rev-parse HEAD` at `$(DATE)`" | tee -a $(INDEX)
-
-dummy: $(PROVER)
-	@echo "Bench started for commit `git rev-parse HEAD` at `$(DATE)`" | tee -a $(INDEX)
-
-$(PROVER): $(SOLVER)
-	@mkdir -p $(LOGDIR)/raw
-	@cp $(SOLVER) $(PROVER)
-
-$(SOLVER):
-	cd .. && $(MAKE)
-
-$(LOGDIR)/raw/%.done : dummy $(PROVER)
-	@mkdir -p $(dir $@)
-	@echo "solving problem $*..." | tee -a $(INDEX)
-	@./run_prover "$(CMD)" "$*" "$@"
-
diff --git a/bench/run_prover b/bench/run_prover
deleted file mode 100755
index 77e420cd..00000000
--- a/bench/run_prover
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/bin/bash
-
-CMD="$1"
-FILE="$2"
-LOG="$3"
-
-/usr/bin/time -f "%e" $CMD $FILE > $3 2>&1
-RET=$?
-if [ $RET -ne 0 ];
-then
-    echo "Error code $RET while solving $FILE"
-fi
diff --git a/util/sat_solve.ml b/main.ml
similarity index 100%
rename from util/sat_solve.ml
rename to main.ml
diff --git a/tests/run b/tests/run
index 99c4613b..4d90b8a3 100755
--- a/tests/run
+++ b/tests/run
@@ -1,7 +1,7 @@
 #!/bin/bash
 
 CURDIR=`dirname $0`
-SOLVER="$CURDIR/../sat_solve.native"
+SOLVER="$CURDIR/../msat"
 
 solvertest () {
     for f in `find -L $1 -type f -name '*.cnf' -o -name '*.smt2'`