diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index c3637bc8f..2def5eaba 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -508,7 +508,7 @@ struct BtorWorker goto okay; } - if (cell->type.in(ID($not), ID($neg), ID($_NOT_), ID($pos))) + if (cell->type.in(ID($not), ID($neg), ID($_NOT_), ID($pos), ID($buf))) { string btor_op; if (cell->type.in(ID($not), ID($_NOT_))) btor_op = "not"; @@ -520,9 +520,9 @@ struct BtorWorker int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); SigSpec sig = sigmap(cell->getPort(ID::Y)); - // the $pos cell just passes through, all other cells need an actual operation applied + // the $pos/$buf cells just pass through, all other cells need an actual operation applied int nid = nid_a; - if (cell->type != ID($pos)) + if (!cell->type.in(ID($pos), ID($buf))) { log_assert(!btor_op.empty()); int sid = get_bv_sid(width);