diff -Naur lingeling-b7ztzu-7b29300-150429/lglib.c lingeling-b7ztzvv-37b745a-150506/lglib.c
--- lingeling-b7ztzu-7b29300-150429/lglib.c	2015-04-27 09:58:22.000000000 +0200
+++ lingeling-b7ztzvv-37b745a-150506/lglib.c	2015-05-06 10:59:40.000000000 +0200
@@ -463,16 +463,6 @@
 
 typedef enum GTag { ANDTAG, ITETAG, XORTAG } GTag;
 
-typedef enum ScrType {
-  STATIC = 0,
-  INC = 1,
-  VMTF = 2,
-  SUM = 3,
-  VSIDS = 4,
-  EVSIDS = 5,
-  AVG = 6,
-} ScrType;
-
 /*------------------------------------------------------------------------*/
 
 typedef int Exp;
@@ -513,7 +503,7 @@
 
 typedef struct DVar { HTS hts[2]; } DVar;
 
-typedef struct QVar { Flt score; int enqueued, prev, next; } QVar;
+typedef struct QVar { int enqueued, prev, next, bumped; } QVar;
 
 typedef struct TD {
   signed int level:30;
@@ -669,7 +659,6 @@
     struct { int64_t total;
 	     struct { int64_t count, sat, unsat; } type[2]; } queries;
   } sweep;
-  struct { int64_t count; int max, min; } setscincf;
   struct { int64_t tried, locked; } promote;
   struct { int count; int64_t quat, self1, self2, dup; } quatres;
   struct {
@@ -824,7 +813,6 @@
 
 typedef struct  Head {
   int first, last, count, unassigned, next;
-  int cache[HEADCACHE], lastenq[HEADCACHE];
 } Head;
 
 typedef struct Queue {
@@ -844,9 +832,6 @@
   int szdrail, next, next2, flushed, level, alevel, wait, glag;
   int unassigned, lrgluereasons, failed, assumed;
 
-  Flt scinc, scincf, maxscore, minscore;
-  int scincinc;
-
   char cceing, gaussing, bcaing, repforcehead, quatres, notrim;
   char searching, simp, allphaseset, flushphases, occs;
   char unhiding, basicprobing, simpleprobing, treelooking, setuponce;
@@ -1013,17 +998,6 @@
   return res;
 }
 
-static Flt lglrat (unsigned n, unsigned d) {
-  Mnt m;
-  Exp e;
-  if (!n) return FLTMIN;
-  if (!d) return FLTMAX;
-  m = n;
-  e = 0;
-  while (!(m & (1ull << 63))) m <<= 1, e--;
-  m /= d;
-  return lglflt (e, m);
-}
 
 #ifndef NDEBUG
 double lglflt2dbl (Flt a) {
@@ -1086,19 +1060,6 @@
   return lglflt (e, m);
 }
 
-static Flt lglshflt (Flt a, int s) {
-  Exp e;
-  Mnt m;
-  if (a == FLTMAX) return FLTMAX;
-  if (a == FLTMIN) return FLTMIN;
-  assert (0 <= s);
-  e = lglexp (a);
-  if (e < INT_MIN + s) return FLTMIN;
-  e -= s;
-  m = lglmnt (a);
-  return lglflt (e, m);
-}
-
 static const char * lglscr2str (LGL * lgl, Flt scr) {
   return lglflt2str (lgl, scr);
 }
@@ -1836,67 +1797,6 @@
   return lgl;
 }
 
-static void lglsetmaxminscore (LGL * lgl) {
-  Flt oldmaxscore = lgl->maxscore, oldminscore = lgl->minscore;
-  lgl->maxscore = lglflt (DEFSCOREXP, 1);
-  lgl->minscore = lglflt (-DEFSCOREXP, 1);
-  if (oldmaxscore != lgl->maxscore)
-    lglprt (lgl, 1,
-      "[set-maximum-score] maximum score limit %s",
-      lglscr2str (lgl, lgl->maxscore));
-  if (oldminscore != lgl->minscore)
-    lglprt (lgl, 1,
-      "[set-minimum-score] minimum score limit %s",
-      lglscr2str (lgl, lgl->minscore));
-}
-
-static void lglsetscincf (LGL * lgl, int scincinc) {
-  assert (lgl->opts->score.val == EVSIDS);
-  if (scincinc == lgl->scincinc) return;
-  lgl->scincf = lglrat (1000 + scincinc, 1000);
-  if (!lgl->stats->setscincf.count++)
-    lgl->stats->setscincf.min = lgl->stats->setscincf.max = scincinc;
-  else {
-    if (scincinc < lgl->stats->setscincf.min)
-      lgl->stats->setscincf.min = scincinc;
-    if (scincinc > lgl->stats->setscincf.max)
-      lgl->stats->setscincf.max = scincinc;
-  }
-  lglprt (lgl, 1,
-    "[set-score-increment-%d] factor %s (%d/1000) after %lld conflicts",
-    lgl->stats->setscincf.count,
-    lglscr2str (lgl, lgl->scincf), scincinc, (LGLL) lgl->stats->confs);
-  lgl->scincinc = scincinc;
-}
-
-static const char *
-lglscortype2str (ScrType st) {
-  switch (st) {
-    case STATIC: return "STATIC";
-    case INC: return "INC";
-    case SUM: return "SUM";
-    case VMTF: return "VMTF";
-    case VSIDS: return "VSIDS";
-    case EVSIDS: return "EVSIDS";
-    case AVG: return "AVG";
-    default: return "UNKNOWN";
-  }
-}
-
-static void lglinitscores (LGL * lgl) {
-  const ScrType st = lgl->opts->score.val;
-  lglsetmaxminscore (lgl);
-  if (st == VSIDS)
-    lglprt (lgl, 1,
-      "[score-type] VSIDS (--score=%d) decay interval %d (--vsidsdint=%d)",
-      st, lgl->opts->vsidsdint.val, lgl->opts->vsidsdint.val);
-  else 
-    lglprt (lgl, 1,
-      "[score-type] %s (--score=%d)",
-      lglscortype2str (st), st);
-  if (st == EVSIDS) lglsetscincf (lgl, lgl->opts->scincinc.val);
-}
-
 LGL * lglminit (void * mem,
 		lglalloc alloc,
 		lglrealloc realloc,
@@ -1951,8 +1851,6 @@
   lglpushstk (lgl, &lgl->wchs->stk, INT_MAX);
   lglpushstk (lgl, &lgl->wchs->stk, INT_MAX);
 
-  lgl->scinc = lglflt (0, 1);
-
   TRANS (UNUSED);
 
   return lgl;
@@ -2409,33 +2307,9 @@
   return lgl->qvars + abs (lit);
 }
 
-/*------------------------------------------------------------------------*/
-
-static int lglscr2exp (LGL * lgl, Flt score) {
-  int res;
-  if (!score) res = 0;
-  else if (score <= lgl->minscore) res = 1;
-  else {
-    res = lglexp (score);
-    assert (-DEFSCOREXP <= res + 32);
-    res += DEFSCOREXP + 32 + 2;
-  }
-  return res;
-}
-
-static int lglscr2cacheidx (Flt score) {
-  Mnt m = score & (MNTBIT - 1);
-  assert (m < MNTBIT);
-  assert (m <= MNTMAX);
-  assert (FLTPRC == 8*MNTBYTES);
-  assert (HEADCACHEBITS <= FLTPRC);
-  m >>= FLTPRC - HEADCACHEBITS;
-  assert (m < HEADCACHE);
-  return (int) m;
-}
-
-static Head * lglhead (LGL * lgl, Flt score) {
-  int exp = lglscr2exp (lgl, score);
+static Head * lglhead (LGL * lgl, int idx) {
+  int exp = lglqvar (lgl, idx)->bumped;
+  assert (0 <= exp), assert (exp <= 1);
   if (exp >= lgl->queue.size) {
     int oldsize = lgl->queue.size;
     int newsize = oldsize ? 2 * oldsize : 1;
@@ -2446,22 +2320,13 @@
   return lgl->queue.heads + exp;
 }
 
-static int lglscrcmp (LGL * lgl, Flt a, Flt b) {
-  const int shift = lgl->opts->scoreshift.val;
-  a >>= shift; assert (a >= 0);
-  b >>= shift; assert (b >= 0);
-  if (a < b) return -1;
-  if (a > b) return 1;
-  return 0;
-}
-
 static int lglisenq (LGL * lgl, int idx) {
   QVar * qv = lglqvar (lgl, idx);
   Head * head;
   int exp, res;
   if (qv->prev) return 1;
   if (qv->next) return 1;
-  exp = lglscr2exp (lgl, qv->score);
+  exp = lglqvar (lgl, idx)->bumped;
   if (exp >= lgl->queue.size) return 0;
   head = lgl->queue.heads + exp;
   res = (head->first == idx);
@@ -2487,11 +2352,10 @@
       val = lglval (lgl, idx);
       fputc (' ', stdout);
       if (idx == h->next) fputc ('<', stdout);
-      printf ("%d=%c:%s",
+      printf ("%d=%c:%d",
 	idx, val < 0 ? 'F' : val ? 'T' : 'X',
-        lglscr2str (lgl, lglqvar (lgl, idx)->score));
+        lglqvar (lgl, idx)->enqueued);
       if (idx == h->next) fputc ('>', stdout);
-      printf ("@%d", lglscr2cacheidx (lglqvar (lgl, idx)->score));
     }
     printf ("\n");
   }
@@ -2505,11 +2369,10 @@
   int exp, total = 0, nextfound;
   for (exp = 0; exp < lgl->queue.size; exp++) {
     Head * h = lgl->queue.heads + exp;
-    int idx, last = 0, count = 0, unassigned = 0, countbackward, cmp;
-    int cacheidx, countcache;
+    int idx, last = 0, count = 0, unassigned = 0, countbackward;
     for (idx = h->first; idx; idx = lglqvar (lgl, idx)->next) {
       QVar * qv = lglqvar (lgl, idx);
-      assert (lglscr2exp (lgl, qv->score) == exp);
+      assert (qv->bumped == exp);
       assert (qv->prev == last);
       if (!lglval (lgl, idx)) unassigned++;
       last = idx;
@@ -2523,9 +2386,7 @@
       assert (qv->next == last);
       if (exp > 0 && last) {
 	QVar * pv = lglqvar (lgl, last);
-	cmp = lglscrcmp (lgl, qv->score, pv->score);
-	assert (cmp <= 0);
-	if (!cmp) assert (qv->enqueued < pv->enqueued);
+	assert (qv->enqueued < pv->enqueued);
       }
       last = idx;
       countbackward++;
@@ -2536,21 +2397,6 @@
     assert (!countbackward || nextfound);
     total += unassigned;
     assert (!unassigned || exp <= lgl->queue.next);
-    countcache = 0;
-    for (cacheidx = 0; cacheidx < HEADCACHE; cacheidx++) {
-      int countline = 0;
-      idx = h->cache[cacheidx];
-      while (idx) {
-	QVar * qv = lglqvar (lgl, idx);
-	int tmp = lglscr2cacheidx (qv->score);
-	assert (tmp <= cacheidx);
-	if (tmp < cacheidx) break;
-	countline++;
-	idx = qv->prev;
-      }
-      countcache += countline;
-    }
-    assert (countcache == h->count);
   }
   assert (!checkunassigned || lgl->unassigned == total);
   total = 0;
@@ -2577,52 +2423,14 @@
 
 static void lglenq (LGL * lgl, int idx) {
   QVar * qv = lglqvar (lgl, idx), * pv;
-  Head * head = lglhead (lgl, qv->score);
-  const int cacheidx = lglscr2cacheidx (qv->score);
-  const int exp = head - lgl->queue.heads;
-  int prev, next, val, cached, lastenq;
+  Head * head = lglhead (lgl, idx);
+  const int exp = qv->bumped;
+  int prev, next, val;
   assert (!lglisenq (lgl, idx));
   assert (!qv->prev), assert (!qv->next);
-  assert (lglscr2exp (lgl, qv->score) == exp);
   lgl->stats->queue.enq.count++;
   prev = head->last;
   if (prev) {
-    int i, steps = 0;
-    for (i = cacheidx; i >= 0 && !(prev = head->cache[i]); i--)
-      ;
-    if (prev) {
-      steps++;
-      pv = lglqvar (lgl, prev);
-      if (lglscrcmp (lgl, pv->score, qv->score) > 0) {
-	if (i == cacheidx && (lastenq = head->lastenq[cacheidx])) {
-	  pv = lglqvar (lgl, lastenq);
-	  if (cacheidx == lglscr2cacheidx (pv->score) && 
-	      lglisenq (lgl, lastenq) &&
-	      lglscrcmp (lgl, pv->score, qv->score) <= 0) {
-	    prev = lastenq;
-	    for (;;) {
-	      next = pv->next;
-	      assert (next);
-	      pv = lglqvar (lgl, next);
-	      assert (lglscr2cacheidx (pv->score) == cacheidx);
-	      if (lglscrcmp (lgl, pv->score, qv->score) > 0) break;
-	      prev = next;
-	    } 
-	    goto FOUND_PREV;
-	  }
-	}
-	while (prev) {
-	  steps++;
-	  pv = lglqvar (lgl, prev);
-	  if (lglscrcmp (lgl, pv->score, qv->score) <= 0) break;
-	  prev = pv->prev;
-	}
-      }
-    }
-FOUND_PREV:
-    lgl->stats->queue.enq.steps += steps;
-  }
-  if (prev) {
     pv = lglqvar (lgl, prev);
     next = pv->next;
     pv->next = idx;
@@ -2642,16 +2450,9 @@
       lgl->queue.next = exp;
     assert (head->unassigned > 0);
   }
-  if (!head->next) head->next = idx;
-  else if (!val && exp > 0) {
-    pv = lglqvar (lgl, head->next);
-    if (lglscrcmp (lgl, pv->score, qv->score) <= 0) head->next = idx;
-  }
+  head->next = idx;
   assert (lgl->enqueued < INT_MAX);
   qv->enqueued = lgl->enqueued++;
-  if (!(cached = head->cache[cacheidx]) || cached == prev)
-    head->cache[cacheidx] = idx;
-  head->lastenq[cacheidx] = idx;
   head->count++;
   if (lgl->enqueued == INT_MAX) lglrecodenqueued (lgl);
 #ifndef NDEBUG
@@ -2661,8 +2462,7 @@
 
 static void lgldeq (LGL * lgl, int idx) {
   QVar * qv = lglqvar (lgl, idx), *pv, * nv;
-  const int exp = lglscr2exp (lgl, qv->score);
-  const int cacheidx = lglscr2cacheidx (qv->score);
+  const int exp = qv->bumped;
   Head * head;
   assert (lglisenq (lgl, idx));
   lgl->stats->queue.deq++;
@@ -2671,16 +2471,6 @@
   assert (head->count > 0);
   if (head->next == idx && !(head->next = qv->prev))
     head->next = (head->last == idx) ? 0 : head->last;
-  if (head->cache[cacheidx] == idx) {
-    int newcachentry = 0;
-    if (qv->prev) {
-      pv = lglqvar (lgl, qv->prev);
-      assert (pv->next == idx);
-      assert (lglscr2cacheidx (pv->score) <= cacheidx);
-      if (lglscr2cacheidx (pv->score) == cacheidx) newcachentry = qv->prev;
-    }
-    head->cache[cacheidx] = newcachentry;
-  }
   if (head->first == idx) head->first = qv->next;
   else {
     assert (qv->prev);
@@ -2708,172 +2498,6 @@
   return 100.0 * n / d;
 }
 
-#define RVL 3
-
-static int lglcmpactive (LGL * lgl, int a, int b) {
-  QVar * qv = lglqvar (lgl, a), * pv = lglqvar (lgl, b);
-  int res = lglscrcmp (lgl, qv->score, pv->score);
-  if (res) return res;
-  return qv->enqueued - pv->enqueued;
-}
-
-#define LGLCMPACTIVE(P,Q) lglcmpactive (lgl, *(P), *(Q))
-
-static void lglrescorevars (LGL * lgl, int full) {
-  Flt oldscinc, oldscore, newscore, oldmaxscore = 0, newmaxscore = 0;
-  int exp, idx, next, * active, nactive, * p, shift;
-  int64_t newotfs;
-  QVar * qv;
-
-  lglstart (lgl, &lgl->times->rescorevars);
-  lgl->stats->rescored.vars++;
-
-  nactive = 0;
-  for (exp = 2; exp < lgl->queue.size; exp++)
-    nactive += lgl->queue.heads[exp].count;
-
-  NEW (active, nactive);
-  lglprt (lgl, RVL,
-    "[rescore-vars-%d] rescoring %d active variables %.0f%%",
-    lgl->stats->rescored.vars, nactive, lglpcnt (nactive, lgl->nvars - 2));
-
-  p = active;
-  for (exp = 2; exp < lgl->queue.size; exp++) {
-    Head * h = lgl->queue.heads + exp;
-    if (!h->count) continue;
-    for (idx = h->first; idx; idx = next) {
-      qv = lglqvar (lgl, idx);
-      next = qv->next;
-      assert (lglscr2exp (lgl, qv->score) == exp);
-      qv->prev = qv->next = 0;
-      assert (p < active + nactive);
-      *p++ = idx;
-    }
-    CLN (h, 1);
-  }
-  assert (p == active + nactive);
-
-  SORT (int, active, nactive, LGLCMPACTIVE);
-
-  lglrecodenqueued (lgl);
-  for (p = active; p < active + nactive; p++) {
-    qv = lglqvar (lgl, *p);
-    assert (lgl->enqueued < INT_MAX);
-    qv->enqueued = lgl->enqueued++;
-  }
-
-  shift = (!full && lgl->opts->score.val == VSIDS) ? 1 : DEFSCOREXP;
-  lglprt (lgl, RVL,
-    "[rescored-vars-%d] dividing scores by 2^%d (right shift by %d)",
-    lgl->stats->rescored.vars, shift, shift);
-
-  for (p = active; p < active + nactive; p++) {
-    idx = *p;
-    qv = lglqvar (lgl, idx);
-    next = qv->next;
-    oldscore = qv->score;
-    if (oldscore > oldmaxscore) oldmaxscore = oldscore;
-    if (oldscore == FLTMIN) newscore = oldscore, assert (!newscore);
-    else if (oldscore <= lgl->minscore) newscore = lgl->minscore;
-    else {
-      newscore = lglshflt (oldscore, shift);
-      if (newscore < lgl->minscore) newscore = lgl->minscore;
-    }
-    if (newscore > newmaxscore) newmaxscore = newscore;
-    qv->score = newscore;
-    LOG (3, "rescored variable %d from %s to %s",
-	 idx, lglscr2str (lgl, oldscore), lglscr2str (lgl, qv->score));
-    lglenq (lgl, idx);
-  }
-
-  DEL (active, nactive);
-
-  newotfs = lgl->stats->otfs.driving + lgl->stats->otfs.restarting;
-  assert (newotfs >= lgl->limits->rescore.vars.otfs);
-  assert (lgl->stats->confs >= lgl->limits->rescore.vars.confs);
-  lglprt (lgl, RVL,
-    "[rescored-vars-%d] after %lld conflicts and %lld OTFS",
-    lgl->stats->rescored.vars,
-    lgl->stats->confs - lgl->limits->rescore.vars.confs,
-    newotfs - lgl->limits->rescore.vars.otfs);
-  lgl->limits->rescore.vars.confs = lgl->stats->confs;
-  lgl->limits->rescore.vars.otfs = newotfs;
-  lglprt (lgl, RVL,
-    "[rescored-vars-%d] old maximum score %s",
-    lgl->stats->rescored.vars, lglscr2str (lgl, oldmaxscore));
-  lglprt (lgl, RVL,
-    "[rescored-vars-%d] new maximum score %s",
-    lgl->stats->rescored.vars, lglscr2str (lgl, newmaxscore));
-  oldscinc = lgl->scinc;
-  if (lgl->opts->score.val != VSIDS)
-    lgl->scinc = lglshflt (oldscinc, shift);
-  assert (lgl->scinc > 0);
-  lglprt (lgl, RVL,
-    "[rescored-vars-%d] old score increment %s",
-    lgl->stats->rescored.vars, lglscr2str (lgl, oldscinc));
-  lglprt (lgl, RVL,
-    "[rescored-vars-%d] new score increment %s",
-    lgl->stats->rescored.vars, lglscr2str (lgl, lgl->scinc));
-
-  lglstop (lgl);
-}
-
-static int lglscincincsatlimok (LGL * lgl);
-
-static void lglbumpscinc (LGL * lgl) {
-  const ScrType st = lgl->opts->score.val;
-  Flt oldscinc, newscinc;
-  if (lgl->simp && !lgl->opts->bumpsimp.val) return;
-  oldscinc = lgl->scinc;
-  switch (st) {
-    case STATIC:
-    case INC:
-    case VMTF:
-    case VSIDS:
-      newscinc = oldscinc;
-      break;
-    case SUM:
-    case AVG:
-      newscinc = lgladdflt (oldscinc, lglflt (0, 1));
-      break;
-    default:
-    case EVSIDS:
-      assert (st == EVSIDS);
-      newscinc = lglmulflt (oldscinc, lgl->scincf);
-      break;
-  }
-  if (st == VSIDS &&
-      !(lgl->stats->confs % lgl->opts->vsidsdint.val)) {
-    lglprt (lgl, 2,
-      "[vsids-decay] halfing scores after %lld conflicts",
-      (LGLL) lgl->stats->confs);
-    lglrescorevars (lgl, 0);
-  }
-  if (newscinc == oldscinc) {
-    LOG (3, "keeping variable score increment at %s",
-      lglscr2str (lgl, lgl->scinc));
-    return;
-  }
-  lgl->scinc = newscinc;
-  LOG (3, "bumped variable score increment from %s to %s",
-       lglscr2str (lgl, oldscinc), lglscr2str (lgl, lgl->scinc));
-  if (lgl->scinc >= lgl->maxscore) {
-    LOG (2, "variable max score %s hit", lglscr2str (lgl, lgl->maxscore));
-    lglrescorevars (lgl, 1);
-  }
-  if (!lgl->simp &&
-      lgl->opts->score.val == EVSIDS &&
-      !(lgl->stats->confs % lgl->opts->scincincincint.val) &&
-      lglscincincsatlimok (lgl)) {
-    int newscincinc = lgl->scincinc;
-    if (lgl->opts->scincincmode.val)
-      newscincinc -= lgl->opts->scincincdelta.val;
-    if (newscincinc < lgl->opts->scincincmin.val)
-      newscincinc = lgl->opts->scincincmin.val;
-    if (newscincinc != lgl->scincinc) lglsetscincf (lgl, newscincinc);
-  }
-}
-
 /*------------------------------------------------------------------------*/
 
 static int lglnewvar (LGL * lgl) {
@@ -2899,7 +2523,7 @@
   CLRPTR (qv);
   lgl->unassigned++;
   lglenq (lgl, res);
-  assert (!lglscr2exp (lgl, qv->score));
+  assert (!qv->bumped);
   assert (lgl->queue.size);
   lgl->queue.heads[0].next = res;
   lgl->allphaseset = 0;
@@ -3322,8 +2946,7 @@
 #endif
 
 static void lglqassign (LGL * lgl, int idx) {
-  QVar * qv = lglqvar (lgl, idx);
-  Head * h = lglhead (lgl, qv->score);
+  Head * h = lglhead (lgl, idx);
   assert (h->unassigned > 0);
   h->unassigned--;
 }
@@ -3496,7 +3119,7 @@
 
 static void lglqunassign (LGL * lgl, int idx) {
   QVar * qv = lglqvar (lgl, idx);
-  int exp = lglscr2exp (lgl, qv->score), cmp;
+  int exp = qv->bumped;
   Head * h;
   assert (exp < lgl->queue.size);
   h = lgl->queue.heads + exp;
@@ -3507,12 +3130,9 @@
   assert (h->next);
   if (exp > 0 && h->next != idx) {
     QVar * pv = lglqvar (lgl, h->next);
-    assert (lglscr2exp (lgl, pv->score) == exp);
-    if ((cmp = lglscrcmp (lgl, pv->score, qv->score)) < 0) {
+    if (pv->enqueued < qv->enqueued) {
       h->next = idx;
-    } else if (!cmp && (pv->enqueued < qv->enqueued)) {
-      h->next = idx;
-    } else assert (cmp > 0 || pv->enqueued > qv->enqueued);
+    } else assert (pv->enqueued > qv->enqueued);
   }
 }
 
@@ -6325,11 +5945,6 @@
 			 lgl->opts->redclsatlimhi.val, 1);
 }
 
-static int lglscincincsatlimok (LGL * lgl) {
-  return lglgensatlimok (lgl, "score inc inc saturating",
-                         0, lgl->opts->scincincsatlimhi.val, 0);
-}
-
 static void lglinitredl (LGL * lgl) {
   lgl->limits->reduce.redlarge = lgl->opts->reduceinit.val;
   lglprt (lgl, 2,
@@ -6878,7 +6493,6 @@
   if (lgl->mt) return;
   lglinitredl (lgl);
   lgliflushcache (lgl, 1);
-  lglinitscores (lgl);
   lglinitredl (lgl);
   lglprt (lgl, 1, "[flush-cache] new limit %d", lgl->limits->reduce.redlarge);
   if (lgl->clone) lglflushcache (lgl->clone);
@@ -7169,34 +6783,16 @@
   lglclnframes (lgl);
 }
 
-static void lglbumpdlit (LGL * lgl, int lit, int * rescoreptr) {
-  const ScrType st = lgl->opts->score.val;
-  Flt oldscore, newscore;
+static void lglbumpdlit (LGL * lgl, int lit) {
+  int oldscore, newscore;
   QVar * qv;
   int idx;
-  assert (st != STATIC);
   idx = abs (lit);
   qv = lglqvar (lgl, idx);
-  oldscore = qv->score;
-  switch (st) {
-    case INC:
-    case SUM:
-    case VSIDS:
-    case EVSIDS:
-      newscore = lgladdflt (oldscore, lgl->scinc);
-      break;
-    case AVG:
-      newscore = lglshflt (lgladdflt (oldscore, lgl->scinc), 1);
-      break;
-    case VMTF:
-    default:
-      assert (st == VMTF);
-      newscore = oldscore;
-      break;
-  }
-  if (newscore < lgl->minscore) newscore = lgl->minscore;
+  oldscore = qv->bumped;
+  newscore = 1;
   assert (newscore >= oldscore);
-  qv->score = newscore;
+  qv->bumped = newscore;
   if (newscore == oldscore)
     LOG (4,
       "keeping score of bumped variable %d at %s",
@@ -7206,39 +6802,33 @@
       "bumping score of variable %d from %s to %s",
       idx, lglscr2str (lgl, oldscore), lglscr2str (lgl, newscore));
   lglenq (lgl, idx);
-  if (newscore >= lgl->maxscore) *rescoreptr = 1;
 }
 
 static int lglcmpbump (LGL * lgl, int a, int b) {
   QVar * qv = lglqvar (lgl, a), * pv = lglqvar (lgl, b);
-  int c = lglscr2exp (lgl, qv->score);
-  int d = lglscr2exp (lgl, pv->score);
+  int c = qv->bumped;
+  int d = pv->bumped;
   int res = c - d;
   if (res) return res;
   assert (c == d);
   assert (c < lgl->queue.size);
-  res = lglscrcmp (lgl, qv->score, pv->score);
-  if (res) return res;
   return qv->enqueued - pv->enqueued;
 }
 
 #define LGLCMPBUMP(P,Q) lglcmpbump (lgl, *(P), *(Q))
 
 static void lglbumpseenlits (LGL * lgl) {
-  int rescore = 0;
   const int * p;
   if (lgl->simp && !lgl->opts->bumpsimp.val) return;
-  if (lgl->opts->score.val == STATIC) return;
   lglstart (lgl, &lgl->times->bump);
   lgl->stats->bump.count++;
   SORT (int, lgl->seen.start, lglcntstk (&lgl->seen), LGLCMPBUMP);
   for (p = lgl->seen.start; p < lgl->seen.top; p++) lgldeq (lgl, abs (*p));
   for (p = lgl->seen.start; p < lgl->seen.top; p++)
-    lglbumpdlit (lgl, *p, &rescore);
+    lglbumpdlit (lgl, *p);
   LOG (2, "bumped %d literals", lglcntstk (&lgl->seen));
   lgl->stats->bump.lits += lglcntstk (&lgl->seen);
   lglstop (lgl);
-  if (rescore) lglrescorevars (lgl, 1);
 #ifndef NDEBUG
   if (lgl->opts->check.val >= 2) lglchkqueue (lgl, 1);
 #endif
@@ -7918,8 +7508,6 @@
   if (uip && lglrsn (lgl, uip)[0]) lgl->stats->uips++;
   else if (jlevel + 1 == lgl->level) lgl->stats->decflipped++;
 
-  lglbumpscinc (lgl);
-
   lglbacktrack (lgl, jlevel);
 
   len = lglcntstk (&lgl->clause) - 1;
@@ -8158,7 +7746,7 @@
     QVar * qv = lglqvar (lgl, res);
     res = qv->prev;
     if (res) continue;
-    assert (lglscr2exp (lgl, qv->score) < 2);
+    assert (!qv->bumped);
     res = h->last;
   }
   h->next = res;
@@ -8169,7 +7757,9 @@
 
 static int lglcmpreusetrail (LGL * lgl, int a, int b) {
   QVar * qv = lglqvar (lgl, a), * pv = lglqvar (lgl, b);
-  return lglscrcmp (lgl, qv->score, pv->score);
+  int res = qv->bumped - pv->bumped;
+  if (res) return res;
+  return qv->enqueued - pv->enqueued;
 }
 
 static int lglreusetrail (LGL * lgl) {
@@ -9042,7 +8632,7 @@
 static void lglmapqueue (LGL * lgl, int * map) {
   int exp;
   for (exp = 0; exp < lgl->queue.size; exp++) {
-    int idx, unassigned, count, cacheidx;
+    int idx, unassigned, count;
     Head * h = lgl->queue.heads + exp;
     QVar * qv;
 
@@ -9056,35 +8646,6 @@
     h->unassigned = unassigned;
     h->count = count;
 
-    for (cacheidx = 0; cacheidx < HEADCACHE; cacheidx++) {
-      int newcachentry = 0;
-      idx = h->cache[cacheidx];
-      while (idx) {
-	QVar * qv = lglqvar (lgl, idx);
-	int tmpcacheidx = lglscr2cacheidx (qv->score);
-	assert (tmpcacheidx <= cacheidx);
-	if (tmpcacheidx < cacheidx) break;
-	if (lglisfree (lgl, idx)) { newcachentry = idx; break; }
-	idx = qv->prev;
-      }
-      assert (!map[0]);
-      h->cache[cacheidx] = map [newcachentry];
-    }
-
-    for (cacheidx = 0; cacheidx < HEADCACHE; cacheidx++) {
-      int newcachentry = 0;
-      idx = h->lastenq[cacheidx];
-      while (idx) {
-	QVar * qv = lglqvar (lgl, idx);
-	int tmpcacheidx = lglscr2cacheidx (qv->score);
-	if (tmpcacheidx != cacheidx) { assert (!newcachentry); break; }
-	if (lglisfree (lgl, idx)) { newcachentry = idx; break; }
-	idx = qv->prev;
-      }
-      assert (!map[0]);
-      h->lastenq[cacheidx] = map [newcachentry];
-    }
-
     idx = h->next;
     while (idx && !lglisfree (lgl, idx))
       idx = lglqvar (lgl, idx)->prev;
@@ -17323,6 +16884,8 @@
   int i, l, k, p, q;
   for (i = 0; i < 4; i++) {
     l = c[i], k = d[i];
+    ASSERT (l != INT_MIN);
+    ASSERT (k != INT_MIN);
     p = abs (l), q = abs (k);
     if (p < q) return -1;
     if (p > q) return 1;
@@ -17595,8 +17158,10 @@
 		glue2 = lidx & GLUEMASK;
 		if (glue2 > maxglue) continue;
 	      } else glue2 = -1;
+	      if (glue2 < glue) continue;
 	      d = lglidx2lits (lgl, red, lidx);
-	      if (d <= c) continue;
+	      if (d == c) continue;
+	      if (glue2 == glue && d < c) continue;
 	      check++;
 	      count = pos = neg = extra = pivot = 0;
 	      for (l = d; (other = *l); l++) {
@@ -17635,13 +17200,26 @@
 		  "2nd pivot %d quaternary scaled glue %d antecedent",
 		  pivot, glue2);
 		LOGCLS (0, lgl->clause.start, "found quaternary resolvent");
+		LOG (5, "before: w + %d = q = eow - %d", (int)(q - w), (int)(eow - w));
 		lgldrupligaddcls (lgl, REDCS);
 		lgladdcls (lgl, REDCS, 4, 0);
 		delta = s->start - start;
-		if (delta) c += delta, p += delta, start = s->start;
+		if (delta) {
+		  LOG (5, "fixing glue %d clauses start by %ld", glue, delta);
+		  c += delta, p += delta, start = s->start;
+		}
 		hts = lglhts (lgl, sign*lit);
 		delta = lglhts2wchs (lgl, hts) - w;
-		if (delta) w += delta, q += delta, eow = w + hts->count;
+		if (delta) {
+		  LOG (5, "fixing %d watches start by %ld", sign*lit, delta);
+		  w += delta, q += delta;
+		}
+		if (w + hts->count != eow) {
+		  LOG (5, "fixing %d watches end from %x to %x",
+		    sign*lit, eow, w + hts->count);
+		  eow = w + hts->count;
+		}
+		LOG (5, "after: w + %d = q = eow - %d", (int)(q - w), (int)(eow - w));
 		lgl->stats->quatres.quat++;
 		*quadptr += 1, quat++;
 	      }
@@ -22168,7 +21746,7 @@
     QVar * qv = lglqvar (lgl, idx);
     next = qv->next;
     qv->prev = qv->next = 0;
-    if (reset) qv->score = 0;
+    if (reset) qv->bumped = 0;
     *p++ = idx;
   }
   CLN (h, 1);
@@ -22872,7 +22450,6 @@
   lgl->setuponce = 1;
   lglchkenv (lgl);
 DONE:
-  lglinitscores (lgl);
   lglincsetup (lgl);
   TRANS (READY);
 }
@@ -24266,12 +23843,6 @@
     lglavg (s->restarts.kept.sum, s->restarts.kept.count));
 
   lglprs (lgl,
-    "scnc: %lld count, %.3f min (%d/1000), %.3f max (%d/1000)",
-    (LGLL) s->setscincf.count,
-    1.0 + s->setscincf.min/1000.0, s->setscincf.min,
-    1.0 + s->setscincf.max/1000.0, s->setscincf.max);
-
-  lglprs (lgl,
     "simp: %d count, %d confs %0.f%%, %d vars %.0f%%",
     s->simp.count,
     s->simp.limhit.confs, lglpcnt (s->simp.limhit.confs, s->simp.count),
diff -Naur lingeling-b7ztzu-7b29300-150429/lgloptl.h lingeling-b7ztzvv-37b745a-150506/lgloptl.h
--- lingeling-b7ztzu-7b29300-150429/lgloptl.h	2015-04-25 21:46:16.000000000 +0200
+++ lingeling-b7ztzvv-37b745a-150506/lgloptl.h	2015-05-06 10:59:40.000000000 +0200
@@ -214,7 +214,6 @@
 OPT(0,scincincincint,100*K,1,I,"score inc inc inc interval");
 OPT(0,scincincmin,200,1,10*K,"min score inc inc in per mille");
 OPT(0,scincincmode,1,0,1,"score inc inc mode (0=keep,1=inc)");
-OPT(0,score,5,0,6,"0=static,1=inc,2=vmtf,3=sum,4=vsids,5=evsids,6=avg");
 OPT(0,scoreshift,0,0,FLTPRC-HEADCACHEBITS,"score shift");
 OPT(0,scoreresetint,I,1,I,"score reset 1 to 0 interval (in queuesort)");
 OPT(0,seed,0,0,I,"random number generator seed");
diff -Naur lingeling-b7ztzu-7b29300-150429/mkconfig.sh lingeling-b7ztzvv-37b745a-150506/mkconfig.sh
--- lingeling-b7ztzu-7b29300-150429/mkconfig.sh	2015-04-29 14:26:58.000000000 +0200
+++ lingeling-b7ztzvv-37b745a-150506/mkconfig.sh	2015-05-06 10:59:43.000000000 +0200
@@ -19,7 +19,7 @@
 echo "#define LGL_OS \"`uname -srmn`\""
 echo "#define LGL_COMPILED \"`date`\""
 cat<<EOF
-#define LGL_RELEASED "Wed Apr 29 14:26:58 CEST 2015"
-#define LGL_VERSION "b7ztzu"
-#define LGL_ID "7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad"
+#define LGL_RELEASED "Wed May  6 10:59:43 CEST 2015"
+#define LGL_VERSION "b7ztzvv"
+#define LGL_ID "37b745a123cb37a24a48e992b1e2073d5d4068bb"
 EOF
diff -Naur lingeling-b7ztzu-7b29300-150429/VERSION lingeling-b7ztzvv-37b745a-150506/VERSION
--- lingeling-b7ztzu-7b29300-150429/VERSION	2015-04-27 09:58:22.000000000 +0200
+++ lingeling-b7ztzvv-37b745a-150506/VERSION	2015-05-06 10:59:40.000000000 +0200
@@ -1 +1 @@
-b7ztzu
+b7ztzvv
