De-prioritize singleton chunks when we know none of them definitely fits

viperproject · Sep 11, 2023 · 9b62b97 · 9b62b97
1 parent 8c0b2d2
commit 9b62b97
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala
@@ -1761,7 +1761,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
         if (greedyMatch.nonEmpty) {
           greedyMatch ++ chunks.diff(greedyMatch)
         } else {
-          fallback(chunks)
+          // It doesn't seem to be any of the singletons. Use the fallback on the non-singletons.
+          val (qpChunks, singletons) = chunks.partition(_.singletonArguments.isEmpty)
+          fallback(qpChunks) ++ singletons
         }
       }
     }