From e5fb9fba290e4a7d2ba5eefe695af44d80623c3f Mon Sep 17 00:00:00 2001
From: George Rennie <georgerennie@gmail.com>
Date: Wed, 20 Nov 2024 13:58:35 +0100
Subject: [PATCH] write_smt2: support $buf and $barrier

---
 backends/smt2/smt2.cc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 40587edae..0685f80eb 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -678,7 +678,7 @@ struct Smt2Worker
 			if (cell->type == ID($eqx)) return export_bvop(cell, "(= A B)", 'b');
 
 			if (cell->type == ID($not)) return export_bvop(cell, "(bvnot A)");
-			if (cell->type == ID($pos)) return export_bvop(cell, "A");
+			if (cell->type.in(ID($pos), ID($buf), ID($barrier))) return export_bvop(cell, "A");
 			if (cell->type == ID($neg)) return export_bvop(cell, "(bvneg A)");
 
 			if (cell->type == ID($add)) return export_bvop(cell, "(bvadd A B)");