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.
YosysHQ · Jun 13, 2023 · c9d31c3 · c9d31c3
1 parent 8b2a001
commit c9d31c3
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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;