From 7764148dd3a247dc1f799dbcdaf67e5a0e7d3443 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 28 Oct 2016 07:42:27 -0700
Subject: [PATCH] merge

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

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 459c11a32..154f3a6a3 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3778,14 +3778,8 @@ namespace smt {
 #ifdef Z3DEBUG
             for (unsigned i = 0; i < num_lits; i++) {
                 literal l = lits[i];
-<<<<<<< HEAD
-                expr* real_atom;
-                if (expr_signs[i] != l.sign()) {
-
-=======
                 if (expr_signs[i] != l.sign()) {
                     expr* real_atom;
->>>>>>> f1412d3f3249529224f4180f601652da210b274a
                     VERIFY(m_manager.is_not(expr_lits.get(i), real_atom));
                     // the sign must have flipped when internalizing
                     CTRACE("resolve_conflict_bug", real_atom != bool_var2expr(l.var()), tout << mk_pp(real_atom, m_manager) << "\n" << mk_pp(bool_var2expr(l.var()), m_manager) << "\n";);