Re-generate response for test-collectiontest

runtimeverification · Nov 27, 2023 · 8e5332b · 8e5332b
1 parent 7e90ecf
commit 8e5332b
Showing 1 changed file with 10 additions and 10 deletions.
diff --git a/test/rpc-integration/test-collectiontest/response-from-12.json b/test/rpc-integration/test-collectiontest/response-from-12.json
@@ -93,7 +93,7 @@
                                                                                                 "name": "SortInt",
                                                                                                 "args": []
                                                                                             },
-                                                                                            "value": "6"
+                                                                                            "value": "4"
                                                                                         }
                                                                                     ]
                                                                                 }
@@ -132,7 +132,7 @@
                                                                                                         "name": "SortInt",
                                                                                                         "args": []
                                                                                                     },
-                                                                                                    "value": "7"
+                                                                                                    "value": "5"
                                                                                                 }
                                                                                             ]
                                                                                         }
@@ -171,7 +171,7 @@
                                                                                                                 "name": "SortInt",
                                                                                                                 "args": []
                                                                                                             },
-                                                                                                            "value": "4"
+                                                                                                            "value": "6"
                                                                                                         }
                                                                                                     ]
                                                                                                 }
@@ -210,7 +210,7 @@
                                                                                                                         "name": "SortInt",
                                                                                                                         "args": []
                                                                                                                     },
-                                                                                                                    "value": "5"
+                                                                                                                    "value": "7"
                                                                                                                 }
                                                                                                             ]
                                                                                                         }
@@ -249,7 +249,7 @@
                                                                                                                                 "name": "SortInt",
                                                                                                                                 "args": []
                                                                                                                             },
-                                                                                                                            "value": "2"
+                                                                                                                            "value": "1"
                                                                                                                         }
                                                                                                                     ]
                                                                                                                 }
@@ -288,7 +288,7 @@
                                                                                                                                         "name": "SortInt",
                                                                                                                                         "args": []
                                                                                                                                     },
-                                                                                                                                    "value": "3"
+                                                                                                                                    "value": "2"
                                                                                                                                 }
                                                                                                                             ]
                                                                                                                         }
@@ -327,7 +327,7 @@
                                                                                                                                                 "name": "SortInt",
                                                                                                                                                 "args": []
                                                                                                                                             },
-                                                                                                                                            "value": "1"
+                                                                                                                                            "value": "3"
                                                                                                                                         }
                                                                                                                                     ]
                                                                                                                                 }
@@ -366,7 +366,7 @@
                                                                                                                                                         "name": "SortInt",
                                                                                                                                                         "args": []
                                                                                                                                                     },
-                                                                                                                                                    "value": "8"
+                                                                                                                                                    "value": "12"
                                                                                                                                                 }
                                                                                                                                             ]
                                                                                                                                         }
@@ -405,7 +405,7 @@
                                                                                                                                                                 "name": "SortInt",
                                                                                                                                                                 "args": []
                                                                                                                                                             },
-                                                                                                                                                            "value": "9"
+                                                                                                                                                            "value": "8"
                                                                                                                                                         }
                                                                                                                                                     ]
                                                                                                                                                 }
@@ -444,7 +444,7 @@
                                                                                                                                                                         "name": "SortInt",
                                                                                                                                                                         "args": []
                                                                                                                                                                     },
-                                                                                                                                                                    "value": "12"
+                                                                                                                                                                    "value": "9"
                                                                                                                                                                 }
                                                                                                                                                             ]
                                                                                                                                                         }