From 57ce615d73995a29f89c2f9b11482fe80442439b Mon Sep 17 00:00:00 2001
From: Kevin Laeufer <laeufer@cs.berkeley.edu>
Date: Fri, 17 Dec 2021 15:04:52 -0500
Subject: [PATCH] smt: correctly serialize array index on read (#2446)

This should fix issue #2436
---
 .../firrtl/backends/experimental/smt/SMTLibSerializer.scala     | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/scala/firrtl/backends/experimental/smt/SMTLibSerializer.scala b/src/main/scala/firrtl/backends/experimental/smt/SMTLibSerializer.scala
index f81acce0050..20a499b9a61 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)})"