Update integration tests

runtimeverification · Aug 7, 2024 · 71998b1 · 71998b1
1 parent 2025987
commit 71998b1
Show file tree

Hide file tree

Showing 11 changed files with 92 additions and 452 deletions.
diff --git a/booster/test/rpc-integration/test-substitutions/README.md b/booster/test/rpc-integration/test-substitutions/README.md
@@ -31,17 +31,16 @@ NB: Booster applies the given substitution before performing any action.
   - with an additional constraint `Y = 1 +Int X` (internalised as a substitution)
   - leading to a contradictory constraint `X = 1 +Int X` after
     rewriting and adding `Y =Int X` from the `ensures`-clause
-    - `kore-rpc-booster` returns `vacuous` after 1 step
-    - `kore-rpc-dev` returns `vacuous` after 0 steps (detects the contradiction earlier)
-    - `kore-rpc-dev` reproduces the exact input as `state` while
-      `kore-rpc-booster` splits off `substitution` (from input) and `predicate` (from the rule)
+    - `kore-rpc-booster` and `booster-dev` return `vacuous` after 0 step, substitution `Y` for `X +Int 1` in the state. However, `kore-rpc-booster` and `booster-dev` disagree a little on the value in the substitution, hence the two responses.
+    - `kore-rpc-dev` returns `vacuous` after 0 steps and reproduces the exact input as `state`
+
 * `state-circular-equations.execute`
   - starts from `concrete-subst`
   - with two equations that have circular dependencies: `Y = 1 +Int X`, `X = Y -Int 1`
   - leading to end state with `X == 42` from the `ensures`-clause
 * `state-symbolic-bottom-predicate.execute`
   - starts from `symbolic-subst`
   - with an equation that is instantly false: `X = 1 +Int X`
-  - leading to a vacuous state in `kore-rpc-booster` after rewriting once,
+  - leading to a vacuous state in `booster-dev` and `kore-rpc-booster`,
   - while `kore-rpc-dev` returns `stuck` instantly after 0 steps,
     returning the exact input as `state`.
diff --git a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev
@@ -225,61 +225,13 @@
                                         }
                                     },
                                     {
-                                        "tag": "App",
-                                        "name": "Lbl'UndsPlus'Int'Unds'",
-                                        "sorts": [],
-                                        "args": [
-                                            {
-                                                "tag": "App",
-                                                "name": "Lbl'UndsPlus'Int'Unds'",
-                                                "sorts": [],
-                                                "args": [
-                                                    {
-                                                        "tag": "EVar",
-                                                        "name": "X",
-                                                        "sort": {
-                                                            "tag": "SortApp",
-                                                            "name": "SortInt",
-                                                            "args": []
-                                                        }
-                                                    },
-                                                    {
-                                                        "tag": "DV",
-                                                        "sort": {
-                                                            "tag": "SortApp",
-                                                            "name": "SortInt",
-                                                            "args": []
-                                                        },
-                                                        "value": "1"
-                                                    }
-                                                ]
-                                            },
-                                            {
-                                                "tag": "App",
-                                                "name": "Lbl'Unds'-Int'Unds'",
-                                                "sorts": [],
-                                                "args": [
-                                                    {
-                                                        "tag": "DV",
-                                                        "sort": {
-                                                            "tag": "SortApp",
-                                                            "name": "SortInt",
-                                                            "args": []
-                                                        },
-                                                        "value": "0"
-                                                    },
-                                                    {
-                                                        "tag": "DV",
-                                                        "sort": {
-                                                            "tag": "SortApp",
-                                                            "name": "SortInt",
-                                                            "args": []
-                                                        },
-                                                        "value": "1"
-                                                    }
-                                                ]
-                                            }
-                                        ]
+                                        "tag": "EVar",
+                                        "name": "X",
+                                        "sort": {
+                                            "tag": "SortApp",
+                                            "name": "SortInt",
+                                            "args": []
+                                        }
                                     }
                                 ]
                             }

diff --git a/...er/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev b/...er/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev