temp = make[xflip];
	make[xflip] = brake[xflip];
	brake[xflip] = temp;

	for (j = 0; j < nYs[xflip]; j++) {
		int y, i, x;

		y = Ys[xflip][j];
		if (X[xflip] != Ysgns[xflip][j]) { 
				/* 'xflip' is no longer satisfying 'y'. */
			sat[y]--;
			if (sat[y] == 0) {
					/* 'y' is newly falsified. */
					/* Need to update all but 'xflip'. */
				yfalse[numvio] = y;
				wherefalse[y] = numvio;
				numvio++;

				for (i = 0; i < nXs[y]; i++) {
					if ((x = Xs[y][i]) != xflip)
						make[x]++;
				}
			} else if (sat[y] == 1) {
							/* Need to update single satisying var. */
				int *Xptr;
				int *Xsgnsyptr;

				Xptr = Xs[y];
				Xsgnsyptr = Xsgns[y];
				x = *Xptr;
				while (*Xsgnsyptr != X[x]) {
					Xptr++;
					Xsgnsyptr++;
					x = *Xptr;
				}
				brake[x]++;
			}
		} else {
				/* 'xflip' is now satisfying 'y'. */
			sat[y]++;
			if (sat[y] == 1) {
					/* 'y' is newly satisfied. */
					/* Need to update all but 'xflip'. */
				numvio--;
				yfalse[wherefalse[y]] = yfalse[numvio];
				wherefalse[yfalse[numvio]] = wherefalse[y];

				for (i = 0; i < nXs[y]; i++)
					if ((x = Xs[y][i]) != xflip)
						make[x]--;
			} else if (sat[y] == 2) {
				int *Xptr;
				int *Xsgnsyptr;

				Xptr = Xs[y];
				Xsgnsyptr = Xsgns[y];
				x = *Xptr;
				while (*Xsgnsyptr != X[x] || x == xflip) {
					Xptr++;
					Xsgnsyptr++;
					x = *Xptr;
				}
				brake[x]--;
			}
		}
	}