From 8a1d67b002d0d0100e97a2c9fc46046e82de2c76 Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Wed, 18 Dec 2024 15:27:38 +0200
Subject: [PATCH] fix mcd proofs
---
tests/specs/mcd-structured/end-pack-pass-rough-spec.k | 3 +++
tests/specs/mcd-structured/flapper-yank-pass-rough-spec.json | 1 +
tests/specs/mcd-structured/flapper-yank-pass-rough-spec.k | 1 +
tests/specs/mcd-structured/vat-spec.json | 1 +
4 files changed, 6 insertions(+)
create mode 100644 tests/specs/mcd-structured/flapper-yank-pass-rough-spec.json
create mode 100644 tests/specs/mcd-structured/vat-spec.json
diff --git a/tests/specs/mcd-structured/end-pack-pass-rough-spec.k b/tests/specs/mcd-structured/end-pack-pass-rough-spec.k
index afb7aa01be..9d59dda3a1 100644
--- a/tests/specs/mcd-structured/end-pack-pass-rough-spec.k
+++ b/tests/specs/mcd-structured/end-pack-pass-rough-spec.k
@@ -191,6 +191,7 @@ module END-PACK-PASS-ROUGH-SPEC
_Vrefund => ?_
_ => ?_
_ => ?_
+ _ => ?_
_
ORIGIN_ID
@@ -293,6 +294,7 @@ module END-PACK-PASS-ROUGH-SPEC
_Vrefund => ?_
_ => ?_
_ => ?_
+ _ => ?_
_
ORIGIN_ID
@@ -395,6 +397,7 @@ module END-PACK-PASS-ROUGH-SPEC
_Vrefund => ?_
_ => ?_
_ => ?_
+ _ => ?_
_
ORIGIN_ID
diff --git a/tests/specs/mcd-structured/flapper-yank-pass-rough-spec.json b/tests/specs/mcd-structured/flapper-yank-pass-rough-spec.json
new file mode 100644
index 0000000000..f48a2390a0
--- /dev/null
+++ b/tests/specs/mcd-structured/flapper-yank-pass-rough-spec.json
@@ -0,0 +1 @@
+{"moduleList": {"node": "KFlatModuleList", "mainModule": "FLAPPER-YANK-PASS-ROUGH-SPEC", "term": [{"node": "KFlatModule", "name": "FLAPPER-YANK-PASS-ROUGH-SPEC", "localSentences": [{"node": "KClaim", "body": {"node": "KApply", "label": {"node": "KLabel", "name": "", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KSequence", "items": [{"node": "KApply", "label": {"node": "KLabel", "name": "execute", "params": []}, "args": [], "arity": 0, "variable": false}, {"node": "KVariable", "name": "CONTINUATION", "sort": {"node": "KSort", "name": "K"}}], "arity": 2}, "rhs": {"node": "KSequence", "items": [{"node": "KApply", "label": {"node": "KLabel", "name": "halt", "params": []}, "args": [], "arity": 0, "variable": false}, {"node": "KVariable", "name": "CONTINUATION", "sort": {"node": "KSort", "name": "K"}}], "arity": 2}}], "arity": 1, "variable": false}, {"node": "KVariable", "name": "_DotVar1", "sort": {"node": "KSort", "name": "ExitCodeCell"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "NORMAL", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "ISTANBUL_EVM", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "", "params": []}, "args": [{"node": "KToken", "token": "true", "sort": {"node": "KSort", "name": "Bool"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "