From 217c0419a13b30d7dcb63cf326cf01aa9a606ce6 Mon Sep 17 00:00:00 2001 From: Mikolas Janota Date: Tue, 29 Mar 2016 19:34:30 +0100 Subject: [PATCH] Avoiding adding a superfluous unary AND in lackr. --- src/ackermannization/lackr.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp index 90c3a7017..b1a58c01b 100644 --- a/src/ackermannization/lackr.cpp +++ b/src/ackermannization/lackr.cpp @@ -109,7 +109,8 @@ bool lackr::ackr(app * const t1, app * const t2) { SASSERT(a1 && a2); TRACE("lackr", tout << "abstr1 " << mk_ismt2_pp(a1, m_m, 2) << "\n";); TRACE("lackr", tout << "abstr2 " << mk_ismt2_pp(a2, m_m, 2) << "\n";); - expr_ref lhs(m_m.mk_and(eqs.size(), eqs.c_ptr()), m_m); + expr_ref lhs(m_m); + lhs = (eqs.size() == 1) ? eqs.get(0) : m_m.mk_and(eqs.size(), eqs.c_ptr()); TRACE("lackr", tout << "ackr constr lhs" << mk_ismt2_pp(lhs, m_m, 2) << "\n";); expr_ref rhs(m_m.mk_eq(a1, a2),m_m); TRACE("lackr", tout << "ackr constr rhs" << mk_ismt2_pp(rhs, m_m, 2) << "\n";);