--- a/src/parallel_execution/MCTaskManagerImpl.h	Thu Jan 28 18:11:53 2021 +0900
+++ b/src/parallel_execution/MCTaskManagerImpl.h	Fri Jan 29 11:55:16 2021 +0900
@@ -13,6 +13,7 @@
   int cpu;
   int gpu;
   int io;
+  int visit;
   int maxCPU;
   __code next(...);
 } MCTaskManagerImpl;

--- a/src/parallel_execution/ModelChecking/MCWorker.cbc	Thu Jan 28 18:11:53 2021 +0900
+++ b/src/parallel_execution/ModelChecking/MCWorker.cbc	Fri Jan 29 11:55:16 2021 +0900
@@ -84,6 +84,7 @@
 extern TaskIterator* createQueueIterator(Element* elements, StateDB s, TaskIterator* prev);
 extern Element* takeNextIterator(TaskIterator* iterator);
 extern void freeIterator(TaskIterator* iterator);
+extern int visit_StateDB(StateDB s, StateDB *parent, StateDB* out, int visit);
 
 
 __ncode mcMeta(struct Context* context, enum Code next) {
@@ -98,7 +99,7 @@
     if (dump) {
         dump_memory(mcti->mem);printf("\n");
     }
-    if (lookup_StateDB(&st, &mcti->state_db, &out)) {
+    if (visit_StateDB(&st, &mcti->state_db, &out,mcti->visit)) {
     // found in the state database
       // printf("found %d\n",count);
       while(!(list = takeNextIterator(mcworker->task_iter))) {
@@ -107,7 +108,11 @@
           if (!prev_iter) {
             printf("All done count %d\n",mcworker->count);
             memory_usage();
-            exit(0);
+            if (mcti->visit == 1) {
+              exit(0);
+            } else {
+              mcti->visit = 1;
+            }
           }
           //printf("no more branch %d\n",count);
           mcworker->depth--;

--- a/src/parallel_execution/ModelChecking/memory.c	Thu Jan 28 18:11:53 2021 +0900
+++ b/src/parallel_execution/ModelChecking/memory.c	Fri Jan 29 11:55:16 2021 +0900
@@ -37,7 +37,7 @@
 
 extern void die_exit(char *);
 
-void 
+void
 die_exit(char *msg)
 {
     fprintf(stderr,"%s\n",msg);
@@ -129,7 +129,7 @@
 
     if (a->adr==b->adr) {
       return 0;
-    } 
+    }
     return (a->adr > b->adr) ? 1 : -1;
 }
 
@@ -159,7 +159,7 @@
     Make a copy of real memory fragments
  */
 
-MemoryPtr 
+MemoryPtr
 copy_memory1(MemoryPtr m)
 {
     MemoryPtr new = create_memory(m->adr,m->length);
@@ -222,7 +222,7 @@
     compute_memory_hash1(m);
     if (m->left)  hash = get_memory_hash(m->left, hash);
     if (m->right) return get_memory_hash(m->right, hash);
-    return m->hash | hash;
+    return (m->hash << 1) ^ hash;
 }
 
 /*
@@ -237,13 +237,13 @@
     m.length = length;
     m.left = m.right = 0;
     compute_memory_hash1(&m);
-    
+
     memory_lookup(&m, parent, copy_memory1, &out);
     return out;
 }
 
 int
-memory_lookup(MemoryPtr m, MemoryPtr *parent, 
+memory_lookup(MemoryPtr m, MemoryPtr *parent,
 		    MemoryPtr (*new_memory)(MemoryPtr), MemoryPtr *out)
 {
     MemoryPtr db;
@@ -287,7 +287,7 @@
     m.adr = ptr;
     m.length = length;
     m.left = m.right = 0;
-    
+
     memory_range_lookup(&m, parent, &out);
     return out;
 }
@@ -296,7 +296,7 @@
 cmp_range(MemoryPtr a,MemoryPtr b)
 {
     if (a->adr==b->adr) {
-      if (a->length != b->length) 
+      if (a->length != b->length)
         die_exit("memory range inconsitency");
       return 0;
     }
@@ -339,7 +339,7 @@
 }
 
 /*
-    dump memory 
+    dump memory
  */
 
 void

--- a/src/parallel_execution/ModelChecking/state_db.c	Thu Jan 28 18:11:53 2021 +0900
+++ b/src/parallel_execution/ModelChecking/state_db.c	Fri Jan 29 11:55:16 2021 +0900
@@ -81,14 +81,13 @@
 }
 
 int
-visit_StateDB(StateDB s, StateDB *parent, int visit)
+visit_StateDB(StateDB s, StateDB *parent, StateDB* out, int visit)
 {
-  StateDB out;
-  lookup__StateDB(s,parent,&out);
-  if (out->visit == visit) {
+  lookup_StateDB(s,parent,out);
+  if ((*out)->visit == visit) {
     return 1;
   }
-  out->visit = visit;
+  (*out)->visit = visit;
   return 0;
  }
 /* end */