mirror of https://github.com/YosysHQ/yosys.git
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.
This commit is contained in:
parent
8b2a001021
commit
c9d31c3c87
|
@ -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;
|
||||
|
|
Loading…
Reference in New Issue