(doh!) fix inc solve flow bug for Marvin Stenger

internal/xo/s.go

@@ -186,10 +186,10 @@ func (s *S) Solve() int {
 		s.assumptLevel = 0
 		s.assumes = s.assumes[:0]
 	}()
+	trail := s.Trail
 	if r := s.solveInit(); r != 0 {
 		return r
 	}
-	trail := s.Trail
 	vars := s.Vars
 	guess := s.Guess
 	guess.nextRestart(s.restartStopwatch)
@@ -480,6 +480,9 @@ func (s *S) Add(m z.Lit) {
 	//s.lock()
 	//defer s.unlock()
 	s.ensureLitCap(m)
+	if m == z.LitNull {
+		s.Trail.Back(s.endTestLevel)
+	}
 	loc, u := s.Cdb.Add(m)
 	if u != z.LitNull {
 		s.Trail.Assign(u, loc)

internal/xo/s_test.go

@@ -4,12 +4,13 @@
 package xo
 
 import (
-	"github.com/irifrance/gini/gen"
-	"github.com/irifrance/gini/z"
 	"log"
 	"math/rand"
 	"testing"
 	"time"
+
+	"github.com/irifrance/gini/gen"
+	"github.com/irifrance/gini/z"
 )
 
 func TestSRand3Cnf(t *testing.T) {
@@ -380,3 +381,23 @@ func TestCopyPause(t *testing.T) {
 	}
 	t.Errorf("giving up, couldn't pause\n")
 }
+
+// Doh!  from Marvin Stenger; thanks!
+func TestIncAdd(t *testing.T) {
+	s := NewS()
+	in, out, x := s.Lit(), s.Lit(), s.Lit()
+	s.Add(in.Not())
+	s.Add(out)
+	s.Add(0)
+	s.Add(in.Not())
+	s.Add(x)
+	s.Add(0)
+	s.Solve()
+	s.Add(in)
+	s.Add(0)
+	s.Add(out)
+	s.Add(0)
+	if s.Solve() != 1 {
+		t.Errorf("unsat")
+	}
+}