From dd786bb5bf4babb7eef988ad3487d627fee13ce4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 14 Jul 2014 15:41:03 +0200 Subject: [PATCH] fix quantifier elimination bugs reported by Berdine and Bornat Signed-off-by: Nikolaj Bjorner --- src/smt/theory_bv.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 44715c37a..8b3021573 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1211,11 +1211,11 @@ namespace smt { } } } - else if (/*m_params.m_bv_enable_int2bv2int &&*/ m_util.is_bv2int(n)) { + else if (m_params.m_bv_enable_int2bv2int && m_util.is_bv2int(n)) { ctx.mark_as_relevant(n->get_arg(0)); assert_bv2int_axiom(n); } - else if (/*m_params.m_bv_enable_int2bv2int &&*/ m_util.is_int2bv(n)) { + else if (m_params.m_bv_enable_int2bv2int && m_util.is_int2bv(n)) { ctx.mark_as_relevant(n->get_arg(0)); assert_int2bv_axiom(n); }