Small tweak to rollback behavior.

src/sat/satoko/solver.c

@@ -397,6 +397,9 @@ static inline void solver_garbage_collect(solver_t *s)
     unsigned *array;
     struct cdb *new_cdb = cdb_alloc(cdb_capacity(s->all_clauses) - cdb_wasted(s->all_clauses));
 
+    if (s->book_cdb)
+        s->book_cdb = 0;
+
     for (i = 0; i < 2 * vec_char_size(s->assigns); i++) {
         struct watcher *w;
         watch_list_foreach(s->watches, w, i)

src/sat/satoko/solver.h

@@ -95,6 +95,7 @@ struct solver_t_ {
     /* Bookmark */
     unsigned book_cl_orig; /* Bookmark for orignal problem clauses vector */
     unsigned book_cl_lrnt; /* Bookmark for learnt clauses vector */
+    unsigned book_cdb;     /* Bookmark clause database size */
     unsigned book_vars;    /* Bookmark number of variables */
     unsigned book_trail;   /* Bookmark trail size */
 

src/sat/satoko/solver_api.c

@@ -330,6 +330,7 @@ void satoko_unbookmark(satoko_t *s)
 {
     s->book_cl_orig = 0;
     s->book_cl_lrnt = 0;
+    s->book_cdb = 0;
     s->book_vars = 0;
     s->book_trail = 0;
 }
@@ -365,6 +366,7 @@ void satoko_reset(satoko_t *s)
     s->RC2 = s->opts.n_conf_fst_reduce;
     s->book_cl_orig = 0;
     s->book_cl_lrnt = 0;
+    s->book_cdb = 0;
     s->book_vars = 0;
     s->book_trail = 0;
 }
@@ -412,6 +414,8 @@ void satoko_rollback(satoko_t *s)
     /* Rewind solver and cancel level 0 assignments to the trail */
     solver_cancel_until(s, 0);
     vec_uint_shrink(s->trail, s->book_trail);
+    if (s->book_cdb)
+        s->all_clauses->size = s->book_cdb;
     s->book_cl_orig = 0;
     s->book_cl_lrnt = 0;
     s->book_vars = 0;