From cf6119cdfd235d36276d9076cabdd0eedf3e4628 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 25 Jan 2019 21:02:25 -0800
Subject: [PATCH] fix #2102

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_seq.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 10b2992fe..6ac1ad4b8 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3148,6 +3148,9 @@ bool theory_seq::solve_nc(unsigned idx) {
         if (!linearize(deps, eqs, lits)) {
             return false;
         }
+        for (literal& lit : lits) {
+            lit.neg();
+        }
         for (enode_pair const& p : eqs) {
             lits.push_back(~mk_eq(p.first->get_owner(), p.second->get_owner(), false));
         }