diff --git a/.unreleased/bug-fixes/1819.md b/.unreleased/bug-fixes/1819.md
new file mode 100644
index 0000000000..2934a56756
--- /dev/null
+++ b/.unreleased/bug-fixes/1819.md
@@ -0,0 +1 @@
+Fix nested set membership in the arrays encoding, see #1819
\ No newline at end of file
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
index 61271f8d8f..2e8194cf3f 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
@@ -331,8 +331,16 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext {
     val (smtEx, _) = toExpr(ex)
     val z3expr = z3solver.getModel.eval(smtEx, true)
     if (z3expr.isBool) {
-      val isTrue = z3expr.getBoolValue.equals(Z3_lbool.Z3_L_TRUE)
-      ValEx(if (isTrue) TlaBool(true) else TlaBool(false)) // in undefined case, just return false
+      z3expr.getBoolValue match {
+        case Z3_lbool.Z3_L_TRUE =>
+          ValEx(TlaBool(true))
+        case Z3_lbool.Z3_L_FALSE =>
+          ValEx(TlaBool(false))
+        case _ =>
+          // If we cannot get a result from evaluating the model, we query the solver
+          z3solver.add(z3expr.asInstanceOf[BoolExpr])
+          ValEx(TlaBool(sat()))
+      }
     } else if (z3expr.isIntNum) {
       ValEx(TlaInt(z3expr.asInstanceOf[IntNum].getBigInteger))
     } else {