#5336

Z3Prover · Jun 17, 2021 · 2174bcc · 2174bcc
1 parent d016cb1
commit 2174bcc
Showing 1 changed file with 4 additions and 6 deletions.
diff --git 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);