diff --git a/booster/test/rpc-integration/test-vacuous/README.md b/booster/test/rpc-integration/test-vacuous/README.md
index bd26765c7c..282675ad7d 100644
--- 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 `bN \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
deleted file mode 100644
index c58212fd42..0000000000
--- a/booster/test/rpc-integration/test-vacuous/params-vacuous-but-rewritten.json
+++ /dev/null
@@ -1 +0,0 @@
-{ "assume-defined": true }
diff --git a/booster/test/rpc-integration/test-vacuous/response-unchecked-vacuous-rewrite.booster-dev b/booster/test/rpc-integration/test-vacuous/response-unchecked-vacuous-rewrite.booster-dev
new file mode 100644
index 0000000000..0737b4680a
--- /dev/null
+++ b/booster/test/rpc-integration/test-vacuous/response-unchecked-vacuous-rewrite.booster-dev
@@ -0,0 +1,215 @@
+{
+ "jsonrpc": "2.0",
+ "id": 1,
+ "result": {
+ "reason": "stuck",
+ "depth": 0,
+ "state": {
+ "term": {
+ "format": "KORE",
+ "version": 1,
+ "term": {
+ "tag": "App",
+ "name": "Lbl'-LT-'generatedTop'-GT-'",
+ "sorts": [],
+ "args": [
+ {
+ "tag": "App",
+ "name": "Lbl'-LT-'k'-GT-'",
+ "sorts": [],
+ "args": [
+ {
+ "tag": "App",
+ "name": "kseq",
+ "sorts": [],
+ "args": [
+ {
+ "tag": "App",
+ "name": "inj",
+ "sorts": [
+ {
+ "tag": "SortApp",
+ "name": "SortState",
+ "args": []
+ },
+ {
+ "tag": "SortApp",
+ "name": "SortKItem",
+ "args": []
+ }
+ ],
+ "args": [
+ {
+ "tag": "DV",
+ "sort": {
+ "tag": "SortApp",
+ "name": "SortState",
+ "args": []
+ },
+ "value": "d"
+ }
+ ]
+ },
+ {
+ "tag": "App",
+ "name": "dotk",
+ "sorts": [],
+ "args": []
+ }
+ ]
+ }
+ ]
+ },
+ {
+ "tag": "App",
+ "name": "Lbl'-LT-'int'-GT-'",
+ "sorts": [],
+ "args": [
+ {
+ "tag": "EVar",
+ "name": "N",
+ "sort": {
+ "tag": "SortApp",
+ "name": "SortInt",
+ "args": []
+ }
+ }
+ ]
+ },
+ {
+ "tag": "App",
+ "name": "Lbl'-LT-'generatedCounter'-GT-'",
+ "sorts": [],
+ "args": [
+ {
+ "tag": "DV",
+ "sort": {
+ "tag": "SortApp",
+ "name": "SortInt",
+ "args": []
+ },
+ "value": "0"
+ }
+ ]
+ }
+ ]
+ }
+ },
+ "predicate": {
+ "format": "KORE",
+ "version": 1,
+ "term": {
+ "tag": "And",
+ "sort": {
+ "tag": "SortApp",
+ "name": "SortGeneratedTopCell",
+ "args": []
+ },
+ "patterns": [
+ {
+ "tag": "Equals",
+ "argSort": {
+ "tag": "SortApp",
+ "name": "SortBool",
+ "args": []
+ },
+ "sort": {
+ "tag": "SortApp",
+ "name": "SortGeneratedTopCell",
+ "args": []
+ },
+ "first": {
+ "tag": "DV",
+ "sort": {
+ "tag": "SortApp",
+ "name": "SortBool",
+ "args": []
+ },
+ "value": "true"
+ },
+ "second": {
+ "tag": "App",
+ "name": "Lbl'UndsEqlsEqls'Int'Unds'",
+ "sorts": [],
+ "args": [
+ {
+ "tag": "EVar",
+ "name": "N",
+ "sort": {
+ "tag": "SortApp",
+ "name": "SortInt",
+ "args": []
+ }
+ },
+ {
+ "tag": "DV",
+ "sort": {
+ "tag": "SortApp",
+ "name": "SortInt",
+ "args": []
+ },
+ "value": "0"
+ }
+ ]
+ }
+ },
+ {
+ "tag": "Equals",
+ "argSort": {
+ "tag": "SortApp",
+ "name": "SortBool",
+ "args": []
+ },
+ "sort": {
+ "tag": "SortApp",
+ "name": "SortGeneratedTopCell",
+ "args": []
+ },
+ "first": {
+ "tag": "DV",
+ "sort": {
+ "tag": "SortApp",
+ "name": "SortBool",
+ "args": []
+ },
+ "value": "true"
+ },
+ "second": {
+ "tag": "App",
+ "name": "LblnotBool'Unds'",
+ "sorts": [],
+ "args": [
+ {
+ "tag": "App",
+ "name": "Lbl'UndsEqlsEqls'Int'Unds'",
+ "sorts": [],
+ "args": [
+ {
+ "tag": "EVar",
+ "name": "N",
+ "sort": {
+ "tag": "SortApp",
+ "name": "SortInt",
+ "args": []
+ }
+ },
+ {
+ "tag": "DV",
+ "sort": {
+ "tag": "SortApp",
+ "name": "SortInt",
+ "args": []
+ },
+ "value": "0"
+ }
+ ]
+ }
+ ]
+ }
+ }
+ ]
+ }
+ }
+ }
+ }
+}
\ No newline at end of file
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
deleted file mode 120000
index bc6397970f..0000000000
--- a/booster/test/rpc-integration/test-vacuous/state-vacuous-but-rewritten.execute
+++ /dev/null
@@ -1 +0,0 @@
-state-vacuous-not-rewritten.execute
\ No newline at end of file
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
deleted file mode 100644
index 0dc921acb0..0000000000
--- a/booster/test/rpc-integration/test-vacuous/state-vacuous-not-rewritten.execute
+++ /dev/null
@@ -1,200 +0,0 @@
-{
- "format": "KORE",
- "version": 1,
- "term": {
- "tag": "And",
- "sort": {
- "tag": "SortApp",
- "name": "SortGeneratedTopCell",
- "args": []
- },
- "first": {
- "tag": "App",
- "name": "Lbl'-LT-'generatedTop'-GT-'",
- "sorts": [],
- "args": [
- {
- "tag": "App",
- "name": "Lbl'-LT-'k'-GT-'",
- "sorts": [],
- "args": [
- {
- "tag": "App",
- "name": "kseq",
- "sorts": [],
- "args": [
- {
- "tag": "App",
- "name": "inj",
- "sorts": [
- {
- "tag": "SortApp",
- "name": "SortState",
- "args": []
- },
- {
- "tag": "SortApp",
- "name": "SortKItem",
- "args": []
- }
- ],
- "args": [
- {
- "tag": "DV",
- "sort": {
- "tag": "SortApp",
- "name": "SortState",
- "args": []
- },
- "value": "b"
- }
- ]
- },
- {
- "tag": "App",
- "name": "dotk",
- "sorts": [],
- "args": []
- }
- ]
- }
- ]
- },
- {
- "tag": "App",
- "name": "Lbl'-LT-'int'-GT-'",
- "sorts": [],
- "args": [
- {
- "tag": "EVar",
- "name": "N",
- "sort": {
- "tag": "SortApp",
- "name": "SortInt",
- "args": []
- }
- }
- ]
- },
- {
- "tag": "App",
- "name": "Lbl'-LT-'generatedCounter'-GT-'",
- "sorts": [],
- "args": [
- {
- "tag": "DV",
- "sort": {
- "tag": "SortApp",
- "name": "SortInt",
- "args": []
- },
- "value": "0"
- }
- ]
- }
- ]
- },
- "second": {
- "tag": "And",
- "sort": {
- "tag": "SortApp",
- "name": "SortGeneratedTopCell",
- "args": []
- },
- "first": {
- "tag": "Equals",
- "sort": {
- "tag": "SortApp",
- "name": "SortGeneratedTopCell",
- "args": []
- },
- "argSort": {
- "tag": "SortApp",
- "name": "SortBool",
- "args": []
- },
- "first": {
- "tag": "App",
- "name": "Lbl'UndsEqlsEqls'Int'Unds'",
- "sorts": [],
- "args": [
- {
- "tag": "EVar",
- "name": "N",
- "sort": {
- "tag": "SortApp",
- "name": "SortInt",
- "args": []
- }
- },
- {
- "tag": "DV",
- "sort": {
- "tag": "SortApp",
- "name": "SortInt",
- "args": []
- },
- "value": "0"
- }
- ]
- },
- "second": {
- "tag": "DV",
- "sort": {
- "tag": "SortApp",
- "name": "SortBool",
- "args": []
- },
- "value": "true"
- }
- },
- "second": {
- "tag": "Equals",
- "sort": {
- "tag": "SortApp",
- "name": "SortGeneratedTopCell",
- "args": []
- },
- "argSort": {
- "tag": "SortApp",
- "name": "SortBool",
- "args": []
- },
- "first": {
- "tag": "App",
- "name": "Lbl'UndsEqlsSlshEqls'Int'Unds'",
- "sorts": [],
- "args": [
- {
- "tag": "EVar",
- "name": "N",
- "sort": {
- "tag": "SortApp",
- "name": "SortInt",
- "args": []
- }
- },
- {
- "tag": "DV",
- "sort": {
- "tag": "SortApp",
- "name": "SortInt",
- "args": []
- },
- "value": "0"
- }
- ]
- },
- "second": {
- "tag": "DV",
- "sort": {
- "tag": "SortApp",
- "name": "SortBool",
- "args": []
- },
- "value": "true"
- }
- }
- }
- }
-}