From 8389465f94cce8a571910c8575d5a87c0b8dbd5c Mon Sep 17 00:00:00 2001
From: aiju <devnull@localhost>
Date: Thu, 22 Mar 2018 13:15:44 +0000
Subject: sat: satget: include unit literals

---
 sys/src/libsat/satget.c | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'sys/src/libsat')

diff --git a/sys/src/libsat/satget.c b/sys/src/libsat/satget.c
index 264311135..72d2789bd 100644
--- a/sys/src/libsat/satget.c
+++ b/sys/src/libsat/satget.c
@@ -8,7 +8,7 @@ satget(SATSolve *s, int i, int *t, int n)
 {
 	SATClause *c;
 	SATLit *l;
-	int j, k;
+	int j, k, m;
 	
 	for(c = s->cl; c != s->learncl; c = c->next)
 		if(i-- == 0){
@@ -23,6 +23,12 @@ satget(SATSolve *s, int i, int *t, int n)
 				if(n > 1) t[1] = signf(l->bimp[k]);
 				return 2;
 			}
+	m = s->lvl == 0 ? s->ntrail : s->decbd[1];
+	for(k = 0; k < m; k++)
+		if(i-- == 0){
+			if(n > 0) t[0] = signf(s->trail[k]);
+			return 1;
+		}
 	for(; c != 0; c = c->next)
 		if(i-- == 0){
 			for(j = 0; j < n && j < c->n; j++)
-- 
cgit v1.2.3