From a22fb8a96e97561b88fc0556b33ac1ec03b9ddb2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Feb 2021 23:11:03 -0800 Subject: [PATCH] revert unit propagation of equality literals Signed-off-by: Nikolaj Bjorner --- src/smt/seq_axioms.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp index 82b71f9a0..6b6d86cb1 100644 --- a/src/smt/seq_axioms.cpp +++ b/src/smt/seq_axioms.cpp @@ -70,7 +70,7 @@ literal seq_axioms::mk_literal(expr* _e) { void seq_axioms::add_clause(expr_ref_vector const& clause) { expr* a = nullptr, *b = nullptr; - if (clause.size() == 1 && m.is_eq(clause[0], a, b)) { + if (false && clause.size() == 1 && m.is_eq(clause[0], a, b)) { enode* n1 = th.ensure_enode(a); enode* n2 = th.ensure_enode(b); justification* js =