git: 9front

Info  •  Files  •  Log  •  Branches

sat: satget: don't duplicate binary clauses

--- a/sys/src/libsat/satget.c

+++ b/sys/src/libsat/satget.c

@@ -18,7 +18,7 @@

 		}

 	for(l = s->lit; l < s->lit + 2 * s->nvar; l++)

 		for(k = 0; k < l->nbimp; k++)

-			if(i-- == 0){

+			if(l - s->lit < l->bimp[k] && i-- == 0){

 				if(n > 0) t[0] = -signf(l - s->lit);

 				if(n > 1) t[1] = signf(l->bimp[k]);

 				return 2;

-- 

⑨