From 2174bccdba73e9ab27adf594378ad5029194e63c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 17 Jun 2021 00:45:52 -0500 Subject: [PATCH] #5336 --- src/sat/smt/bv_internalize.cpp | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index deadc5a630a..e3c193f5a6a 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -661,12 +661,10 @@ namespace bv { if (lit0 == sat::null_literal) { m_bits[v_arg][idx] = lit; TRACE("bv", tout << "add-bit: " << lit << " " << literal2expr(lit) << "\n";); - if (arg_sz > 1) { - atom* a = new (get_region()) atom(lit.var()); - a->m_occs = new (get_region()) var_pos_occ(v_arg, idx); - insert_bv2a(lit.var(), a); - ctx.push(mk_atom_trail(lit.var(), *this)); - } + atom* a = new (get_region()) atom(lit.var()); + a->m_occs = new (get_region()) var_pos_occ(v_arg, idx); + insert_bv2a(lit.var(), a); + ctx.push(mk_atom_trail(lit.var(), *this)); } else if (lit != lit0) { add_clause(lit0, ~lit);