summaryrefslogtreecommitdiff
path: root/sys/src/libsat
diff options
context:
space:
mode:
authoraiju <devnull@localhost>2018-03-22 13:35:52 +0000
committeraiju <devnull@localhost>2018-03-22 13:35:52 +0000
commit39dd26bf0807046b8c9824745751248db3bf2de0 (patch)
treeff6c3eb084238021bd536fbda6eea4fcf99e36e0 /sys/src/libsat
parent8389465f94cce8a571910c8575d5a87c0b8dbd5c (diff)
sat: satget: don't duplicate binary clauses
Diffstat (limited to 'sys/src/libsat')
-rw-r--r--sys/src/libsat/satget.c2
1 files changed, 1 insertions, 1 deletions
diff --git a/sys/src/libsat/satget.c b/sys/src/libsat/satget.c
index 72d2789bd..ae5f5ccec 100644
--- a/sys/src/libsat/satget.c
+++ b/sys/src/libsat/satget.c
@@ -18,7 +18,7 @@ satget(SATSolve *s, int i, int *t, int n)
}
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;