fix: Z3 seems to repeat some keys in the statistics. Lets avoid this …

…issue by renaming the keys in the statistics.

Actually, using Map as signature for statistics maybe was a non-optimal choice,
because several solvers only provide plain text without any structure.

This bug was noticed in hernanponcedeleon/Dat3M#221,
but it was never officially reported to JavaSMT.

src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java

@@ -21,6 +21,7 @@
 import java.util.ArrayList;
 import java.util.Collection;
 import java.util.HashMap;
+import java.util.HashSet;
 import java.util.List;
 import java.util.Map;
 import java.util.Map.Entry;
@@ -264,10 +265,11 @@ public ImmutableMap<String, String> getStatistics() {
     Preconditions.checkState(!closed);
 
     ImmutableMap.Builder<String, String> builder = ImmutableMap.builder();
+    Set<String> seenKeys = new HashSet<>();
 
     final long stats = Native.solverGetStatistics(z3context, z3solver);
     for (int i = 0; i < Native.statsSize(z3context, stats); i++) {
-      String key = Native.statsGetKey(z3context, stats, i);
+      String key = getUnusedKey(seenKeys, Native.statsGetKey(z3context, stats, i));
       if (Native.statsIsUint(z3context, stats, i)) {
         builder.put(key, Integer.toString(Native.statsGetUintValue(z3context, stats, i)));
       } else if (Native.statsIsDouble(z3context, stats, i)) {
@@ -283,6 +285,23 @@ public ImmutableMap<String, String> getStatistics() {
     return builder.buildOrThrow();
   }
 
+  /**
+   * In some cases, Z3 uses the same statistics key twice. In those cases, we append an index to the
+   * second usage.
+   */
+  private String getUnusedKey(Set<String> seenKeys, final String originalKey) {
+    if (seenKeys.add(originalKey)) {
+      return originalKey;
+    }
+    String key;
+    int index = 0;
+    do {
+      index++;
+      key = originalKey + " (" + index + ")";
+    } while (!seenKeys.add(key));
+    return key;
+  }
+
   @Override
   public void close() {
     if (!closed) {