From d7c66889052854a40d577e8d216c328256cd869a Mon Sep 17 00:00:00 2001 From: George Rennie Date: Fri, 15 Nov 2024 11:47:09 +0100 Subject: [PATCH] write_btor: support $_BUF_ --- backends/btor/btor.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 2def5eaba..ad8f4b680 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), ID($buf))) + if (cell->type.in(ID($not), ID($neg), ID($_NOT_), ID($pos), ID($buf), ID($_BUF_))) { string btor_op; if (cell->type.in(ID($not), ID($_NOT_))) btor_op = "not"; @@ -522,7 +522,7 @@ struct BtorWorker // the $pos/$buf cells just pass through, all other cells need an actual operation applied int nid = nid_a; - if (!cell->type.in(ID($pos), ID($buf))) + if (!cell->type.in(ID($pos), ID($buf), ID($_BUF_))) { log_assert(!btor_op.empty()); int sid = get_bv_sid(width);