From 58be5e28b1bf852396871e7f4b1c465ea4a796dc Mon Sep 17 00:00:00 2001
From: Scott <wsc@iri-labs.com>
Date: Sat, 8 Sep 2018 16:46:53 +0200
Subject: [PATCH] (doh!) fix inc solve flow bug for Marvin Stenger

---
 internal/xo/s.go      |  5 ++++-
 internal/xo/s_test.go | 25 +++++++++++++++++++++++--
 2 files changed, 27 insertions(+), 3 deletions(-)

diff --git a/internal/xo/s.go b/internal/xo/s.go
index a9717ba..aea8e64 100644
--- a/internal/xo/s.go
+++ b/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)
diff --git a/internal/xo/s_test.go b/internal/xo/s_test.go
index d71b500..d4a1e76 100644
--- a/internal/xo/s_test.go
+++ b/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")
+	}
+}