Regression test for long running z3 commands (#2814)

* Add regression-test * Update regression-tests * Add golden-output
runtimeverification · Sep 6, 2021 · ac02ece · ac02ece
1 parent 6dab583
commit ac02ece
Show file tree

Hide file tree

Showing 29 changed files with 75,711 additions and 20,072 deletions.
diff --git a/scripts/generate-regression-tests.sh b/scripts/generate-regression-tests.sh
@@ -94,6 +94,9 @@ generate-evm() {
     kollect test-totalSupply \
         make tests/specs/erc20/ds/totalSupply-spec.k.prove -s -e
 
+    kollect test-addu48u48 \
+        make tests/specs/mcd/flipper-addu48u48-fail-rough-spec.k.prove -s -e
+
     $KORE/scripts/trim-source-paths.sh *.kore
 }
 

diff --git a/test/regression-evm/test-add0-definition.kore b/test/regression-evm/test-add0-definition.kore
diff --git a/test/regression-evm/test-addu48u48-spec.kore b/test/regression-evm/test-addu48u48-spec.kore
diff --git a/test/regression-evm/test-addu48u48-vdefinition.kore b/test/regression-evm/test-addu48u48-vdefinition.kore
diff --git a/test/regression-evm/test-addu48u48.sh b/test/regression-evm/test-addu48u48.sh
@@ -0,0 +1,2 @@
+#!/bin/sh
+${KORE_EXEC:?} test-addu48u48-vdefinition.kore --module VERIFICATION --prove test-addu48u48-spec.kore --spec-module FLIPPER-ADDU48U48-FAIL-ROUGH-SPEC "$@"
diff --git a/test/regression-evm/test-addu48u48.sh.out.golden b/test/regression-evm/test-addu48u48.sh.out.golden
@@ -0,0 +1 @@
+/* D Sfa */ \top{R}()
diff --git a/test/regression-evm/test-and0-definition.kore b/test/regression-evm/test-and0-definition.kore
diff --git a/test/regression-evm/test-branching-invalid-definition.kore b/test/regression-evm/test-branching-invalid-definition.kore
diff --git a/test/regression-evm/test-branching-no-invalid-definition.kore b/test/regression-evm/test-branching-no-invalid-definition.kore
diff --git a/test/regression-evm/test-lemmas-spec.kore b/test/regression-evm/test-lemmas-spec.kore
diff --git a/test/regression-evm/test-lemmas-vdefinition.kore b/test/regression-evm/test-lemmas-vdefinition.kore
diff --git a/test/regression-evm/test-mul0-definition.kore b/test/regression-evm/test-mul0-definition.kore
diff --git a/test/regression-evm/test-pop1-definition.kore b/test/regression-evm/test-pop1-definition.kore
diff --git a/test/regression-evm/test-sha3_bigSize-definition.kore b/test/regression-evm/test-sha3_bigSize-definition.kore
diff --git a/test/regression-evm/test-storagevar03-vdefinition.kore b/test/regression-evm/test-storagevar03-vdefinition.kore
diff --git a/test/regression-evm/test-straight-line-definition.kore b/test/regression-evm/test-straight-line-definition.kore
diff --git a/test/regression-evm/test-straight-line-no-invalid-definition.kore b/test/regression-evm/test-straight-line-no-invalid-definition.kore
diff --git a/test/regression-evm/test-sum-to-n-spec.kore b/test/regression-evm/test-sum-to-n-spec.kore
diff --git a/test/regression-evm/test-sum-to-n-vdefinition.kore b/test/regression-evm/test-sum-to-n-vdefinition.kore
diff --git a/test/regression-evm/test-sumTo10-definition.kore b/test/regression-evm/test-sumTo10-definition.kore
diff --git a/test/regression-evm/test-totalSupply-vdefinition.kore b/test/regression-evm/test-totalSupply-vdefinition.kore
diff --git a/test/regression-wasm/test-locals-vdefinition.kore b/test/regression-wasm/test-locals-vdefinition.kore
diff --git a/test/regression-wasm/test-loops-spec.kore b/test/regression-wasm/test-loops-spec.kore
diff --git a/test/regression-wasm/test-loops-vdefinition.kore b/test/regression-wasm/test-loops-vdefinition.kore
diff --git a/test/regression-wasm/test-memory-spec.kore b/test/regression-wasm/test-memory-spec.kore
diff --git a/test/regression-wasm/test-memory-vdefinition.kore b/test/regression-wasm/test-memory-vdefinition.kore
diff --git a/test/regression-wasm/test-simple-arithmetic-spec.kore b/test/regression-wasm/test-simple-arithmetic-spec.kore
@@ -6,15 +6,15 @@ import KWASM-LEMMAS []
 
 
 // claims
-// claim `<generatedTop>`(`<wasm>`(`<instrs>`(inj{PlainInstr,KItem}(aIConst(ITYPE,inj{Int,WasmInt}(X)))~>inj{PlainInstr,KItem}(aIConst(ITYPE,inj{Int,WasmInt}(Y)))~>inj{PlainInstr,KItem}(aIBinOp(ITYPE,intAdd(.KList)))~>_DotVar2),`<valstack>`(S),_0,_1,_2,_3,_4,_5,_6),_DotVar0)=>`<generatedTop>`(`<wasm>`(`<instrs>`(_DotVar2),`<valstack>`(`_:__WASM-DATA_ValStack_Val_ValStack`(inj{IVal,Val}(`<_>__WASM-DATA_IVal_IValType_Int`(ITYPE,`_+Int_`(X,Y))),S)),_0,_1,_2,_3,_4,_5,_6),_DotVar0) requires `_andBool_`(`_andBool_`(`_<=Int_`(#token("0","Int"),X),`_<=Int_`(#token("0","Int"),Y)),`_<Int_`(`_+Int_`(X,Y),`#pow(_)_WASM-DATA_Int_IValType`(ITYPE))) ensures #token("true","Bool") [org.kframework.attributes.Location(Location(14,11,17,44)), org.kframework.attributes.Source(Source(wasm-semantics/tests/proofs/simple-arithmetic-spec.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])]
+// claim `<generatedTop>`(`<wasm>`(`<instrs>`(inj{PlainInstr,KItem}(aIConst(ITYPE,inj{Int,WasmInt}(X)))~>_DotVar2),`<valstack>`(S),_0,_1,_2,_3,_4,_5,_6),_DotVar0)=>`<generatedTop>`(`<wasm>`(`<instrs>`(_DotVar2),`<valstack>`(`_:__WASM-DATA_ValStack_Val_ValStack`(inj{IVal,Val}(`<_>__WASM-DATA_IVal_IValType_Int`(ITYPE,X)),S)),_0,_1,_2,_3,_4,_5,_6),_DotVar0) requires `#inUnsignedRange(_,_)_KWASM-LEMMAS_Bool_IValType_Int`(ITYPE,X) ensures #token("true","Bool") [org.kframework.attributes.Location(Location(6,11,8,43)), org.kframework.attributes.Source(Source(wasm-semantics/tests/proofs/simple-arithmetic-spec.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])]
   claim{} \implies{SortGeneratedTopCell{}} (
       \and{SortGeneratedTopCell{}} (
       \equals{SortBool{},SortGeneratedTopCell{}}(
-        Lbl'Unds'andBool'Unds'{}(Lbl'Unds'andBool'Unds'{}(Lbl'Unds-LT-Eqls'Int'Unds'{}(\dv{SortInt{}}("0"),VarX:SortInt{}),Lbl'Unds-LT-Eqls'Int'Unds'{}(\dv{SortInt{}}("0"),VarY:SortInt{})),Lbl'Unds-LT-'Int'Unds'{}(Lbl'UndsPlus'Int'Unds'{}(VarX:SortInt{},VarY:SortInt{}),Lbl'Hash'pow'LParUndsRParUnds'WASM-DATA'Unds'Int'Unds'IValType{}(VarITYPE:SortIValType{}))),
-        \dv{SortBool{}}("true")), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'wasm'-GT-'{}(Lbl'-LT-'instrs'-GT-'{}(kseq{}(inj{SortPlainInstr{}, SortKItem{}}(LblaIConst{}(VarITYPE:SortIValType{},inj{SortInt{}, SortWasmInt{}}(VarX:SortInt{}))),kseq{}(inj{SortPlainInstr{}, SortKItem{}}(LblaIConst{}(VarITYPE:SortIValType{},inj{SortInt{}, SortWasmInt{}}(VarY:SortInt{}))),kseq{}(inj{SortPlainInstr{}, SortKItem{}}(LblaIBinOp{}(VarITYPE:SortIValType{},LblintAdd{}())),Var'Unds'DotVar2:SortK{})))),Lbl'-LT-'valstack'-GT-'{}(VarS:SortValStack{}),Var'Unds'0:SortCurFrameCell{},Var'Unds'1:SortModuleRegistryCell{},Var'Unds'2:SortModuleIdsCell{},Var'Unds'3:SortModuleInstancesCell{},Var'Unds'4:SortNextModuleIdxCell{},Var'Unds'5:SortMainStoreCell{},Var'Unds'6:SortDeterministicMemoryGrowthCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{})), weakAlwaysFinally{SortGeneratedTopCell{}} (
+        Lbl'Hash'inUnsignedRange'LParUndsCommUndsRParUnds'KWASM-LEMMAS'Unds'Bool'Unds'IValType'Unds'Int{}(VarITYPE:SortIValType{},VarX:SortInt{}),
+        \dv{SortBool{}}("true")), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'wasm'-GT-'{}(Lbl'-LT-'instrs'-GT-'{}(kseq{}(inj{SortPlainInstr{}, SortKItem{}}(LblaIConst{}(VarITYPE:SortIValType{},inj{SortInt{}, SortWasmInt{}}(VarX:SortInt{}))),Var'Unds'DotVar2:SortK{})),Lbl'-LT-'valstack'-GT-'{}(VarS:SortValStack{}),Var'Unds'0:SortCurFrameCell{},Var'Unds'1:SortModuleRegistryCell{},Var'Unds'2:SortModuleIdsCell{},Var'Unds'3:SortModuleInstancesCell{},Var'Unds'4:SortNextModuleIdxCell{},Var'Unds'5:SortMainStoreCell{},Var'Unds'6:SortDeterministicMemoryGrowthCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{})), weakAlwaysFinally{SortGeneratedTopCell{}} (
       \and{SortGeneratedTopCell{}} (
-      \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'wasm'-GT-'{}(Lbl'-LT-'instrs'-GT-'{}(Var'Unds'DotVar2:SortK{}),Lbl'-LT-'valstack'-GT-'{}(Lbl'UndsColnUndsUnds'WASM-DATA'Unds'ValStack'Unds'Val'Unds'ValStack{}(inj{SortIVal{}, SortVal{}}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}(VarITYPE:SortIValType{},Lbl'UndsPlus'Int'Unds'{}(VarX:SortInt{},VarY:SortInt{}))),VarS:SortValStack{})),Var'Unds'0:SortCurFrameCell{},Var'Unds'1:SortModuleRegistryCell{},Var'Unds'2:SortModuleIdsCell{},Var'Unds'3:SortModuleInstancesCell{},Var'Unds'4:SortNextModuleIdxCell{},Var'Unds'5:SortMainStoreCell{},Var'Unds'6:SortDeterministicMemoryGrowthCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{}))))
-  [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(14,11,17,44)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(wasm-semantics/tests/proofs/simple-arithmetic-spec.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}()]
+      \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'wasm'-GT-'{}(Lbl'-LT-'instrs'-GT-'{}(Var'Unds'DotVar2:SortK{}),Lbl'-LT-'valstack'-GT-'{}(Lbl'UndsColnUndsUnds'WASM-DATA'Unds'ValStack'Unds'Val'Unds'ValStack{}(inj{SortIVal{}, SortVal{}}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}(VarITYPE:SortIValType{},VarX:SortInt{})),VarS:SortValStack{})),Var'Unds'0:SortCurFrameCell{},Var'Unds'1:SortModuleRegistryCell{},Var'Unds'2:SortModuleIdsCell{},Var'Unds'3:SortModuleInstancesCell{},Var'Unds'4:SortNextModuleIdxCell{},Var'Unds'5:SortMainStoreCell{},Var'Unds'6:SortDeterministicMemoryGrowthCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{}))))
+  [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(6,11,8,43)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(wasm-semantics/tests/proofs/simple-arithmetic-spec.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}()]
 
 // claim `<generatedTop>`(`<wasm>`(`<instrs>`(inj{PlainInstr,KItem}(aIConst(ITYPE,inj{Int,WasmInt}(X)))~>_DotVar2),`<valstack>`(S),_0,_1,_2,_3,_4,_5,_6),_DotVar0)=>`<generatedTop>`(`<wasm>`(`<instrs>`(_DotVar2),`<valstack>`(`_:__WASM-DATA_ValStack_Val_ValStack`(inj{IVal,Val}(`<_>__WASM-DATA_IVal_IValType_Int`(ITYPE,`_+Int_`(X,`#pow(_)_WASM-DATA_Int_IValType`(ITYPE)))),S)),_0,_1,_2,_3,_4,_5,_6),_DotVar0) requires `_andBool_`(`_<=Int_`(`#minSigned(_)_KWASM-LEMMAS_Int_IValType`(ITYPE),X),`_<Int_`(X,#token("0","Int"))) ensures #token("true","Bool") [org.kframework.attributes.Location(Location(10,11,12,63)), org.kframework.attributes.Source(Source(wasm-semantics/tests/proofs/simple-arithmetic-spec.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])]
   claim{} \implies{SortGeneratedTopCell{}} (
@@ -26,14 +26,14 @@ import KWASM-LEMMAS []
       \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'wasm'-GT-'{}(Lbl'-LT-'instrs'-GT-'{}(Var'Unds'DotVar2:SortK{}),Lbl'-LT-'valstack'-GT-'{}(Lbl'UndsColnUndsUnds'WASM-DATA'Unds'ValStack'Unds'Val'Unds'ValStack{}(inj{SortIVal{}, SortVal{}}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}(VarITYPE:SortIValType{},Lbl'UndsPlus'Int'Unds'{}(VarX:SortInt{},Lbl'Hash'pow'LParUndsRParUnds'WASM-DATA'Unds'Int'Unds'IValType{}(VarITYPE:SortIValType{})))),VarS:SortValStack{})),Var'Unds'0:SortCurFrameCell{},Var'Unds'1:SortModuleRegistryCell{},Var'Unds'2:SortModuleIdsCell{},Var'Unds'3:SortModuleInstancesCell{},Var'Unds'4:SortNextModuleIdxCell{},Var'Unds'5:SortMainStoreCell{},Var'Unds'6:SortDeterministicMemoryGrowthCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{}))))
   [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(10,11,12,63)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(wasm-semantics/tests/proofs/simple-arithmetic-spec.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}()]
 
-// claim `<generatedTop>`(`<wasm>`(`<instrs>`(inj{PlainInstr,KItem}(aIConst(ITYPE,inj{Int,WasmInt}(X)))~>_DotVar2),`<valstack>`(S),_0,_1,_2,_3,_4,_5,_6),_DotVar0)=>`<generatedTop>`(`<wasm>`(`<instrs>`(_DotVar2),`<valstack>`(`_:__WASM-DATA_ValStack_Val_ValStack`(inj{IVal,Val}(`<_>__WASM-DATA_IVal_IValType_Int`(ITYPE,X)),S)),_0,_1,_2,_3,_4,_5,_6),_DotVar0) requires `#inUnsignedRange(_,_)_KWASM-LEMMAS_Bool_IValType_Int`(ITYPE,X) ensures #token("true","Bool") [org.kframework.attributes.Location(Location(6,11,8,43)), org.kframework.attributes.Source(Source(wasm-semantics/tests/proofs/simple-arithmetic-spec.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])]
+// claim `<generatedTop>`(`<wasm>`(`<instrs>`(inj{PlainInstr,KItem}(aIConst(ITYPE,inj{Int,WasmInt}(X)))~>inj{PlainInstr,KItem}(aIConst(ITYPE,inj{Int,WasmInt}(Y)))~>inj{PlainInstr,KItem}(aIBinOp(ITYPE,intAdd(.KList)))~>_DotVar2),`<valstack>`(S),_0,_1,_2,_3,_4,_5,_6),_DotVar0)=>`<generatedTop>`(`<wasm>`(`<instrs>`(_DotVar2),`<valstack>`(`_:__WASM-DATA_ValStack_Val_ValStack`(inj{IVal,Val}(`<_>__WASM-DATA_IVal_IValType_Int`(ITYPE,`_+Int_`(X,Y))),S)),_0,_1,_2,_3,_4,_5,_6),_DotVar0) requires `_andBool_`(`_andBool_`(`_<=Int_`(#token("0","Int"),X),`_<=Int_`(#token("0","Int"),Y)),`_<Int_`(`_+Int_`(X,Y),`#pow(_)_WASM-DATA_Int_IValType`(ITYPE))) ensures #token("true","Bool") [org.kframework.attributes.Location(Location(14,11,17,44)), org.kframework.attributes.Source(Source(wasm-semantics/tests/proofs/simple-arithmetic-spec.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])]
   claim{} \implies{SortGeneratedTopCell{}} (
       \and{SortGeneratedTopCell{}} (
       \equals{SortBool{},SortGeneratedTopCell{}}(
-        Lbl'Hash'inUnsignedRange'LParUndsCommUndsRParUnds'KWASM-LEMMAS'Unds'Bool'Unds'IValType'Unds'Int{}(VarITYPE:SortIValType{},VarX:SortInt{}),
-        \dv{SortBool{}}("true")), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'wasm'-GT-'{}(Lbl'-LT-'instrs'-GT-'{}(kseq{}(inj{SortPlainInstr{}, SortKItem{}}(LblaIConst{}(VarITYPE:SortIValType{},inj{SortInt{}, SortWasmInt{}}(VarX:SortInt{}))),Var'Unds'DotVar2:SortK{})),Lbl'-LT-'valstack'-GT-'{}(VarS:SortValStack{}),Var'Unds'0:SortCurFrameCell{},Var'Unds'1:SortModuleRegistryCell{},Var'Unds'2:SortModuleIdsCell{},Var'Unds'3:SortModuleInstancesCell{},Var'Unds'4:SortNextModuleIdxCell{},Var'Unds'5:SortMainStoreCell{},Var'Unds'6:SortDeterministicMemoryGrowthCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{})), weakAlwaysFinally{SortGeneratedTopCell{}} (
+        Lbl'Unds'andBool'Unds'{}(Lbl'Unds'andBool'Unds'{}(Lbl'Unds-LT-Eqls'Int'Unds'{}(\dv{SortInt{}}("0"),VarX:SortInt{}),Lbl'Unds-LT-Eqls'Int'Unds'{}(\dv{SortInt{}}("0"),VarY:SortInt{})),Lbl'Unds-LT-'Int'Unds'{}(Lbl'UndsPlus'Int'Unds'{}(VarX:SortInt{},VarY:SortInt{}),Lbl'Hash'pow'LParUndsRParUnds'WASM-DATA'Unds'Int'Unds'IValType{}(VarITYPE:SortIValType{}))),
+        \dv{SortBool{}}("true")), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'wasm'-GT-'{}(Lbl'-LT-'instrs'-GT-'{}(kseq{}(inj{SortPlainInstr{}, SortKItem{}}(LblaIConst{}(VarITYPE:SortIValType{},inj{SortInt{}, SortWasmInt{}}(VarX:SortInt{}))),kseq{}(inj{SortPlainInstr{}, SortKItem{}}(LblaIConst{}(VarITYPE:SortIValType{},inj{SortInt{}, SortWasmInt{}}(VarY:SortInt{}))),kseq{}(inj{SortPlainInstr{}, SortKItem{}}(LblaIBinOp{}(VarITYPE:SortIValType{},LblintAdd{}())),Var'Unds'DotVar2:SortK{})))),Lbl'-LT-'valstack'-GT-'{}(VarS:SortValStack{}),Var'Unds'0:SortCurFrameCell{},Var'Unds'1:SortModuleRegistryCell{},Var'Unds'2:SortModuleIdsCell{},Var'Unds'3:SortModuleInstancesCell{},Var'Unds'4:SortNextModuleIdxCell{},Var'Unds'5:SortMainStoreCell{},Var'Unds'6:SortDeterministicMemoryGrowthCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{})), weakAlwaysFinally{SortGeneratedTopCell{}} (
       \and{SortGeneratedTopCell{}} (
-      \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'wasm'-GT-'{}(Lbl'-LT-'instrs'-GT-'{}(Var'Unds'DotVar2:SortK{}),Lbl'-LT-'valstack'-GT-'{}(Lbl'UndsColnUndsUnds'WASM-DATA'Unds'ValStack'Unds'Val'Unds'ValStack{}(inj{SortIVal{}, SortVal{}}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}(VarITYPE:SortIValType{},VarX:SortInt{})),VarS:SortValStack{})),Var'Unds'0:SortCurFrameCell{},Var'Unds'1:SortModuleRegistryCell{},Var'Unds'2:SortModuleIdsCell{},Var'Unds'3:SortModuleInstancesCell{},Var'Unds'4:SortNextModuleIdxCell{},Var'Unds'5:SortMainStoreCell{},Var'Unds'6:SortDeterministicMemoryGrowthCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{}))))
-  [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(6,11,8,43)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(wasm-semantics/tests/proofs/simple-arithmetic-spec.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}()]
+      \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'wasm'-GT-'{}(Lbl'-LT-'instrs'-GT-'{}(Var'Unds'DotVar2:SortK{}),Lbl'-LT-'valstack'-GT-'{}(Lbl'UndsColnUndsUnds'WASM-DATA'Unds'ValStack'Unds'Val'Unds'ValStack{}(inj{SortIVal{}, SortVal{}}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}(VarITYPE:SortIValType{},Lbl'UndsPlus'Int'Unds'{}(VarX:SortInt{},VarY:SortInt{}))),VarS:SortValStack{})),Var'Unds'0:SortCurFrameCell{},Var'Unds'1:SortModuleRegistryCell{},Var'Unds'2:SortModuleIdsCell{},Var'Unds'3:SortModuleInstancesCell{},Var'Unds'4:SortNextModuleIdxCell{},Var'Unds'5:SortMainStoreCell{},Var'Unds'6:SortDeterministicMemoryGrowthCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{}))))
+  [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(14,11,17,44)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(wasm-semantics/tests/proofs/simple-arithmetic-spec.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}()]
 
 endmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(3,1,18,9)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(wasm-semantics/tests/proofs/simple-arithmetic-spec.k)")]
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		#!/bin/sh
		${KORE_EXEC:?} test-addu48u48-vdefinition.kore --module VERIFICATION --prove test-addu48u48-spec.kore --spec-module FLIPPER-ADDU48U48-FAIL-ROUGH-SPEC "$@"