diff options
| author | Kevin Laeufer | 2021-12-17 15:04:52 -0500 |
|---|---|---|
| committer | GitHub | 2021-12-17 12:04:52 -0800 |
| commit | 57ce615d73995a29f89c2f9b11482fe80442439b (patch) | |
| tree | c7e967091d98272443d1890fcb1fd6d516364137 | |
| parent | 37c8528cfed4395924820b54498ef761ded17393 (diff) | |
smt: correctly serialize array index on read (#2446)
This should fix issue #2436
| -rw-r--r-- | src/main/scala/firrtl/backends/experimental/smt/SMTLibSerializer.scala | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/main/scala/firrtl/backends/experimental/smt/SMTLibSerializer.scala b/src/main/scala/firrtl/backends/experimental/smt/SMTLibSerializer.scala index f81acce0..20a499b9 100644 --- a/src/main/scala/firrtl/backends/experimental/smt/SMTLibSerializer.scala +++ b/src/main/scala/firrtl/backends/experimental/smt/SMTLibSerializer.scala @@ -70,7 +70,7 @@ object SMTLibSerializer { case BVOp(op, a, b) if a.width == 1 => toBool(s"(${serialize(op)} ${asBitVector(a)} ${asBitVector(b)})") case BVOp(op, a, b) => s"(${serialize(op)} ${serialize(a)} ${serialize(b)})" case BVConcat(a, b) => s"(concat ${asBitVector(a)} ${asBitVector(b)})" - case ArrayRead(array, index) => s"(select ${serialize(array)} ${asBitVector(index)})" + case ArrayRead(array, index) => s"(select ${serialize(array)} ${serialize(index)})" case BVIte(cond, tru, fals) => s"(ite ${serialize(cond)} ${serialize(tru)} ${serialize(fals)})" case BVFunctionCall(name, args, _) => args.map(serializeArg).mkString(s"($name ", " ", ")") case BVForall(variable, e) => s"(forall ((${variable.name} ${serialize(variable.tpe)})) ${serialize(e)})" |