X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fmain.c;h=45831e7d2cbadddfbf0995db630f35066226d2bf;hb=363cf737b04fbeab89362b6252b97db10d25ca02;hp=1fd9e93f4c9f5b5eaea7ff21ca206a22f7062c25;hpb=2be3ea1fc484406a2865426c9b02ad7e9ff703ba;p=mc1516pa.git

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 1fd9e93..45831e7 100644
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -7,6 +7,7 @@
 #include <sylvan.h>
 
 #include "sokoban.h"
+#include "coord.h"
 
 #define ERRPRINT(fmt, as...) fprintf(stderr, fmt, ## as);
 #define DPRINT(fmt, as...) if(DEBUG) ERRPRINT(fmt, ## as);
@@ -47,18 +48,20 @@ void solve(FILE *inputstream)
 	sokoban_screen *screen = parse_screen(inputstream);
 	if (screen == NULL) printf("Something went wrong...\n");
 	sokoban_print(screen);
-	sokoban_free(screen);
 
 	time_end_read = clock();
 	time_start_encode = clock();
-	
+
 	lace_init(0, 1000000);
 	lace_startup(0, NULL, NULL);
 	LACE_ME;
     sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
     sylvan_init_bdd(6);
-	
-	//ENCODE???
+
+	encode_screen(screen);
+
+	sokoban_free(screen);
+
 	switch(strat){
 		case COORD:
 			DPRINT("Encoding coordinate based\n");