From 71d80ab47f21a07a54cdf61366a7028df82488d3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 31 Jul 2017 11:54:11 -0700
Subject: [PATCH] fix build break based on new assertion in
 smt-eq-justification

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

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 76d8a5a74..e72cd3f6d 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1681,6 +1681,7 @@ bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector cons
         bool has_conflict = false;
         for (unsigned j = 0; !has_conflict && j < sz; ++j) {
             unsigned j1 = (offset + j) % sz;
+            if (xs[j] == ys[j1]) continue;
             literal eq = mk_eq(xs[j], ys[j1], false);
             switch (ctx.get_assignment(eq)) {
             case l_false: