Reorganize tests

runtimeverification · Aug 21, 2024 · 2ad1c79 · 2ad1c79
1 parent e155e58
commit 2ad1c79
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 202 deletions.
diff --git a/booster/test/rpc-integration/test-vacuous/README.md b/booster/test/rpc-integration/test-vacuous/README.md
@@ -47,5 +47,15 @@ Rules `init` and `AC` introduce constraints on this variable:
    _Expected:_
    - The state is simplified and discovered to be `vacuous` (with state `b`).
 
+1) _unchecked-vacuous-rewritten_
+
+   _Input:_ same as _vacuous-not-rewritten_
+   - `execute` request with initial state  `<k>b</k><int>N</int> \and N
+     ==Int 1  \and N =/=Int  1` (A contradiction in the initial constraints).
+
+   _Expected:_
+   - the input constraints are not checked for satisfiability (`"assume-defined": true` is in params)
+   - one rewrite step is made and the result is `stuck`
+
 With `kore-rpc-dev`, some contradictions will be discovered before or while
 attempting to rewrite (at the time of writing, it returns `stuck`, though).
diff --git a/booster/test/rpc-integration/test-vacuous/params-vacuous-but-rewritten.json b/booster/test/rpc-integration/test-vacuous/params-vacuous-but-rewritten.json
diff --git a/booster/test/rpc-integration/test-vacuous/state-vacuous-but-rewritten.execute b/booster/test/rpc-integration/test-vacuous/state-vacuous-but-rewritten.execute
diff --git a/booster/test/rpc-integration/test-vacuous/state-vacuous-not-rewritten.execute b/booster/test/rpc-integration/test-vacuous/state-vacuous-not-rewritten.execute