Merge branch 'main' into igor/z3-thread-fix

apalache-mc · Oct 4, 2024 · be05b3a · be05b3a
2 parents fb11296 + 9e9d099
commit be05b3a
Showing 1 changed file with 3 additions and 12 deletions.
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
@@ -776,27 +776,18 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL
         } else {
           val (es, ns) = (args.map(toExpr)).unzip
           val distinct = z3context.mkDistinct(es: _*)
-          (distinct.asInstanceOf[ExprSort],
-              ns.foldLeft(1L) {
-                _ + _
-              })
+          (distinct.asInstanceOf[ExprSort], ns.sum + 1)
         }
 
       case OperEx(TlaBoolOper.and, args @ _*) =>
         val (es, ns) = (args.map(toExpr)).unzip
         val and = z3context.mkAnd(es.map(_.asInstanceOf[BoolExpr]): _*)
-        (and.asInstanceOf[ExprSort],
-            ns.foldLeft(1L) {
-              _ + _
-            })
+        (and.asInstanceOf[ExprSort], ns.sum + 1)
 
       case OperEx(TlaBoolOper.or, args @ _*) =>
         val (es, ns) = (args.map(toExpr)).unzip
         val or = z3context.mkOr(es.map(_.asInstanceOf[BoolExpr]): _*)
-        (or.asInstanceOf[ExprSort],
-            ns.foldLeft(1L) {
-              _ + _
-            })
+        (or.asInstanceOf[ExprSort], ns.sum + 1)
 
       case OperEx(TlaBoolOper.implies, lhs, rhs) =>
         val (lhsZ3, ln) = toExpr(lhs)