From c9d31c3c876c1b95accede88cbe8687eab815e7f Mon Sep 17 00:00:00 2001 From: Charlotte Connor Date: Tue, 13 Jun 2023 14:59:18 +1000 Subject: [PATCH] smt2: abits needs to be at least 1 for BitVec BitVecs need a minimum length of 1; we zero-fill any extra bits in the extend_u0() calls which works perfectly. --- backends/smt2/smt2.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 7b48be29902..5e63e62370d 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -773,7 +773,7 @@ struct Smt2Worker int arrayid = idcounter++; memarrays[mem] = arrayid; - int abits = ceil_log2(mem->size); + int abits = max(1, ceil_log2(mem->size)); bool has_sync_wr = false; bool has_async_wr = false; @@ -1220,7 +1220,7 @@ struct Smt2Worker { int arrayid = memarrays.at(mem); - int abits = ceil_log2(mem->size);; + int abits = max(1, ceil_log2(mem->size)); bool has_sync_wr = false; bool has_async_wr = false;