write_smt2: support $buf and $barrier

georgerennie · Nov 20, 2024 · 70e1381 · 70e1381
1 parent 5c24f73
commit 70e1381
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
@@ -677,7 +677,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)");