From 62b8394bdd6fdb4dcdb634aa2055692095265786 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 31 Jul 2017 09:52:45 -0700 Subject: [PATCH] fixes #1179 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_justification.h | 1 + src/smt/theory_seq.cpp | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_justification.h b/src/smt/smt_justification.h index ea969d1db..f4b3ecb12 100644 --- a/src/smt/smt_justification.h +++ b/src/smt/smt_justification.h @@ -181,6 +181,7 @@ namespace smt { enode * m_node2; public: eq_propagation_justification(enode * n1, enode * n2):m_node1(n1), m_node2(n2) { + SASSERT(n1 != n2); } virtual void get_antecedents(conflict_resolution & cr); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 832995994..76d8a5a74 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1891,7 +1891,7 @@ bool theory_seq::solve_ne(unsigned idx) { new_ls.push_back(ls); new_rs.push_back(rs); } - else { + else if (nl != nr) { literal lit(mk_eq(nl, nr, false)); ctx.mark_as_relevant(lit); new_lits.push_back(lit);