Skip to content

Commit 2ad1c79

Browse files
committed
Reorganize tests
1 parent e155e58 commit 2ad1c79

File tree

4 files changed

+10
-202
lines changed

4 files changed

+10
-202
lines changed

booster/test/rpc-integration/test-vacuous/README.md

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,5 +47,15 @@ Rules `init` and `AC` introduce constraints on this variable:
4747
_Expected:_
4848
- The state is simplified and discovered to be `vacuous` (with state `b`).
4949

50+
1) _unchecked-vacuous-rewritten_
51+
52+
_Input:_ same as _vacuous-not-rewritten_
53+
- `execute` request with initial state `<k>b</k><int>N</int> \and N
54+
==Int 1 \and N =/=Int 1` (A contradiction in the initial constraints).
55+
56+
_Expected:_
57+
- the input constraints are not checked for satisfiability (`"assume-defined": true` is in params)
58+
- one rewrite step is made and the result is `stuck`
59+
5060
With `kore-rpc-dev`, some contradictions will be discovered before or while
5161
attempting to rewrite (at the time of writing, it returns `stuck`, though).

booster/test/rpc-integration/test-vacuous/params-vacuous-but-rewritten.json

Lines changed: 0 additions & 1 deletion
This file was deleted.

booster/test/rpc-integration/test-vacuous/state-vacuous-but-rewritten.execute

Lines changed: 0 additions & 1 deletion
This file was deleted.

booster/test/rpc-integration/test-vacuous/state-vacuous-not-rewritten.execute

Lines changed: 0 additions & 200 deletions
This file was deleted.

0 commit comments

Comments
 (0)