diff --git a/package/version b/package/version
index 1ec9b0b64..a2d633db7 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.60
+0.1.61
diff --git a/pyproject.toml b/pyproject.toml
index 014456d27..6f3fa6e27 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.60"
+version = "0.1.61"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
index ce29fa190..66278d984 100644
--- a/src/kontrol/__init__.py
+++ b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.60'
+VERSION: Final = '0.1.61'
diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py
index fd4ef354b..70ea6c355 100644
--- a/src/kontrol/solc_to_k.py
+++ b/src/kontrol/solc_to_k.py
@@ -410,11 +410,11 @@ def srcmap(self) -> dict[int, tuple[int, int, int, str, int]]:
 
     @staticmethod
     def contract_to_module_name(c: str) -> str:
-        return c + '-CONTRACT'
+        return Contract.escaped(c, 'S2K') + '-CONTRACT'
 
     @staticmethod
     def contract_to_verification_module_name(c: str) -> str:
-        return c + '-VERIFICATION'
+        return Contract.escaped(c, 'S2K') + '-VERIFICATION'
 
     @staticmethod
     def test_to_claim_name(t: str) -> str:
@@ -426,7 +426,7 @@ def name_upper(self) -> str:
 
     @staticmethod
     def escaped_chars() -> list[str]:
-        return [Contract.PREFIX_CODE, '_', '$']
+        return [Contract.PREFIX_CODE, '_', '$', '.']
 
     @staticmethod
     def escape_char(char: str) -> str:
@@ -437,6 +437,8 @@ def escape_char(char: str) -> str:
                 as_ecaped = 'Und'
             case '$':
                 as_ecaped = 'Dlr'
+            case '.':
+                as_ecaped = 'Dot'
             case _:
                 as_ecaped = hex(ord(char)).removeprefix('0x')
         return f'{Contract.PREFIX_CODE}{as_ecaped}'
@@ -449,6 +451,8 @@ def unescape_seq(seq: str) -> tuple[str, int]:
             return '_', 3
         elif seq.startswith('Dlr'):
             return '$', 3
+        elif seq.startswith('Dot'):
+            return '.', 3
         else:
             return chr(int(seq, base=16)), 4
 
diff --git a/src/tests/integration/test-data/contracts.k.expected b/src/tests/integration/test-data/contracts.k.expected
index 6d41964be..18e634800 100644
--- a/src/tests/integration/test-data/contracts.k.expected
+++ b/src/tests/integration/test-data/contracts.k.expected
@@ -1,6 +1,6 @@
 requires "foundry.md"
 
-module AccountParamsTest-CONTRACT
+module S2KAccountParamsTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KAccountParamsTestContract
@@ -283,7 +283,7 @@ module AccountParamsTest-CONTRACT
 
 endmodule
 
-module AddrTest-CONTRACT
+module S2KAddrTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KAddrTestContract
@@ -540,7 +540,7 @@ module AddrTest-CONTRACT
 
 endmodule
 
-module AllowChangesTest-CONTRACT
+module S2KAllowChangesTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KAllowChangesTestContract
@@ -771,7 +771,7 @@ module AllowChangesTest-CONTRACT
 
 endmodule
 
-module ValueStore-CONTRACT
+module S2KValueStore-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KValueStoreContract
@@ -833,7 +833,7 @@ module ValueStore-CONTRACT
 
 endmodule
 
-module AmbiguousTest-CONTRACT
+module S2KAmbiguousTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KAmbiguousTestContract
@@ -889,7 +889,7 @@ module AmbiguousTest-CONTRACT
 
 endmodule
 
-module ArithmeticTest-CONTRACT
+module S2KArithmeticTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KArithmeticTestContract
@@ -1215,7 +1215,7 @@ module ArithmeticTest-CONTRACT
 
 endmodule
 
-module AssumeTest-CONTRACT
+module S2KAssumeTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KAssumeTestContract
@@ -1462,7 +1462,7 @@ module AssumeTest-CONTRACT
 
 endmodule
 
-module BMCLoopsTest-CONTRACT
+module S2KBMCLoopsTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KBMCLoopsTestContract
@@ -1671,7 +1671,7 @@ module BMCLoopsTest-CONTRACT
 
 endmodule
 
-module CommonBase-CONTRACT
+module S2KCommonBase-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KCommonBaseContract
@@ -1692,7 +1692,7 @@ module CommonBase-CONTRACT
 
 endmodule
 
-module ScriptBase-CONTRACT
+module S2KScriptBase-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KScriptBaseContract
@@ -1713,7 +1713,7 @@ module ScriptBase-CONTRACT
 
 endmodule
 
-module TestBase-CONTRACT
+module S2KTestBase-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KTestBaseContract
@@ -1734,7 +1734,7 @@ module TestBase-CONTRACT
 
 endmodule
 
-module BlockParamsTest-CONTRACT
+module S2KBlockParamsTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KBlockParamsTestContract
@@ -1969,7 +1969,7 @@ module BlockParamsTest-CONTRACT
 
 endmodule
 
-module RollTest-CONTRACT
+module S2KRollTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KRollTestContract
@@ -2168,7 +2168,7 @@ module RollTest-CONTRACT
 
 endmodule
 
-module BroadcastTest-CONTRACT
+module S2KBroadcastTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KBroadcastTestContract
@@ -2393,7 +2393,7 @@ module BroadcastTest-CONTRACT
 
 endmodule
 
-module Constants-CONTRACT
+module S2KConstants-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KConstantsContract
@@ -2407,7 +2407,7 @@ module Constants-CONTRACT
 
 endmodule
 
-module Contract-CONTRACT
+module S2KContract-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KContractContract
@@ -2421,7 +2421,7 @@ module Contract-CONTRACT
 
 endmodule
 
-module ContractTest-CONTRACT
+module S2KContractTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KContractTestContract
@@ -2612,7 +2612,7 @@ module ContractTest-CONTRACT
 
 endmodule
 
-module ContractBTest-CONTRACT
+module S2KContractBTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KContractBTestContract
@@ -2832,7 +2832,7 @@ module ContractBTest-CONTRACT
 
 endmodule
 
-module Counter-CONTRACT
+module S2KCounter-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KCounterContract
@@ -2880,7 +2880,7 @@ module Counter-CONTRACT
 
 endmodule
 
-module CounterTest-CONTRACT
+module S2KCounterTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KCounterTestContract
@@ -3101,7 +3101,7 @@ module CounterTest-CONTRACT
 
 endmodule
 
-module DynamicTypes-CONTRACT
+module S2KDynamicTypes-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KDynamicTypesContract
@@ -3295,7 +3295,7 @@ module DynamicTypes-CONTRACT
 
 endmodule
 
-module ExpectEmit-CONTRACT
+module S2KExpectEmit-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KExpectEmitContract
@@ -3319,7 +3319,7 @@ module ExpectEmit-CONTRACT
 
 endmodule
 
-module EmitContractTest-CONTRACT
+module S2KEmitContractTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KEmitContractTestContract
@@ -3526,7 +3526,7 @@ module EmitContractTest-CONTRACT
 
 endmodule
 
-module EnvTest-CONTRACT
+module S2KEnvTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KEnvTestContract
@@ -3821,7 +3821,7 @@ module EnvTest-CONTRACT
 
 endmodule
 
-module Dummy-CONTRACT
+module S2KDummy-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KDummyContract
@@ -3845,7 +3845,7 @@ module Dummy-CONTRACT
 
 endmodule
 
-module ExpectCallTest-CONTRACT
+module S2KExpectCallTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KExpectCallTestContract
@@ -4052,7 +4052,7 @@ module ExpectCallTest-CONTRACT
 
 endmodule
 
-module DepthReverter-CONTRACT
+module S2KDepthReverter-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KDepthReverterContract
@@ -4083,7 +4083,7 @@ module DepthReverter-CONTRACT
 
 endmodule
 
-module ExpectRevertTest-CONTRACT
+module S2KExpectRevertTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KExpectRevertTestContract
@@ -4363,7 +4363,7 @@ module ExpectRevertTest-CONTRACT
 
 endmodule
 
-module Reverter-CONTRACT
+module S2KReverter-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KReverterContract
@@ -4403,7 +4403,7 @@ module Reverter-CONTRACT
 
 endmodule
 
-module ReverterWithReturn-CONTRACT
+module S2KReverterWithReturn-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KReverterWithReturnContract
@@ -4437,7 +4437,7 @@ module ReverterWithReturn-CONTRACT
 
 endmodule
 
-module FfiTest-CONTRACT
+module S2KFfiTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KFfiTestContract
@@ -4660,7 +4660,7 @@ module FfiTest-CONTRACT
 
 endmodule
 
-module FilesTest-CONTRACT
+module S2KFilesTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KFilesTestContract
@@ -4867,7 +4867,7 @@ module FilesTest-CONTRACT
 
 endmodule
 
-module ForkTest-CONTRACT
+module S2KForkTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KForkTestContract
@@ -5130,7 +5130,7 @@ module ForkTest-CONTRACT
 
 endmodule
 
-module FreshIntTest-CONTRACT
+module S2KFreshIntTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KFreshIntTestContract
@@ -5353,7 +5353,7 @@ module FreshIntTest-CONTRACT
 
 endmodule
 
-module GasTest-CONTRACT
+module S2KGasTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KGasTestContract
@@ -5560,7 +5560,7 @@ module GasTest-CONTRACT
 
 endmodule
 
-module GetCodeTest-CONTRACT
+module S2KGetCodeTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KGetCodeTestContract
@@ -5764,7 +5764,7 @@ module GetCodeTest-CONTRACT
 
 endmodule
 
-module IMulticall3-CONTRACT
+module S2KIMulticall3-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KIMulticall3Contract
@@ -5892,7 +5892,7 @@ module IMulticall3-CONTRACT
 
 endmodule
 
-module InitCodeTest-CONTRACT
+module S2KInitCodeTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KInitCodeTestContract
@@ -6114,7 +6114,7 @@ module InitCodeTest-CONTRACT
 
 endmodule
 
-module InitCodeBranchTest-CONTRACT
+module S2KInitCodeBranchTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KInitCodeBranchTestContract
@@ -6323,7 +6323,7 @@ module InitCodeBranchTest-CONTRACT
 
 endmodule
 
-module KEVMCheats-CONTRACT
+module S2KKEVMCheats-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KKEVMCheatsContract
@@ -6347,7 +6347,7 @@ module KEVMCheats-CONTRACT
 
 endmodule
 
-module KEVMCheatsBase-CONTRACT
+module S2KKEVMCheatsBase-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KKEVMCheatsBaseContract
@@ -6503,7 +6503,7 @@ module KEVMCheatsBase-CONTRACT
 
 endmodule
 
-module LabelTest-CONTRACT
+module S2KLabelTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KLabelTestContract
@@ -6694,7 +6694,7 @@ module LabelTest-CONTRACT
 
 endmodule
 
-module LoopsTest-CONTRACT
+module S2KLoopsTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KLoopsTestContract
@@ -7016,7 +7016,7 @@ module LoopsTest-CONTRACT
 
 endmodule
 
-module MergeTest-CONTRACT
+module S2KMergeTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KMergeTestContract
@@ -7221,7 +7221,7 @@ module MergeTest-CONTRACT
 
 endmodule
 
-module MethodDisambiguateTest-CONTRACT
+module S2KMethodDisambiguateTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KMethodDisambiguateTestContract
@@ -7430,7 +7430,7 @@ module MethodDisambiguateTest-CONTRACT
 
 endmodule
 
-module MockCallTest-CONTRACT
+module S2KMockCallTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KMockCallTestContract
@@ -7637,7 +7637,7 @@ module MockCallTest-CONTRACT
 
 endmodule
 
-module MyIERC20-CONTRACT
+module S2KMyIERC20-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KMyIERC20Contract
@@ -7720,7 +7720,7 @@ module MyIERC20-CONTRACT
 
 endmodule
 
-module MyToken-CONTRACT
+module S2KMyToken-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KMyTokenContract
@@ -7783,7 +7783,7 @@ module MyToken-CONTRACT
 
 endmodule
 
-module NoImport-CONTRACT
+module S2KNoImport-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KNoImportContract
@@ -7807,7 +7807,7 @@ module NoImport-CONTRACT
 
 endmodule
 
-module OwnerUpOnly-CONTRACT
+module S2KOwnerUpOnly-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KOwnerUpOnlyContract
@@ -7854,7 +7854,7 @@ module OwnerUpOnly-CONTRACT
 
 endmodule
 
-module OwnerUpOnlyTest-CONTRACT
+module S2KOwnerUpOnlyTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KOwnerUpOnlyTestContract
@@ -8074,7 +8074,7 @@ module OwnerUpOnlyTest-CONTRACT
 
 endmodule
 
-module AdditionalToken-CONTRACT
+module S2KAdditionalToken-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KAdditionalTokenContract
@@ -8121,7 +8121,7 @@ module AdditionalToken-CONTRACT
 
 endmodule
 
-module MyErc20-CONTRACT
+module S2KMyErc20-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KMyErc20Contract
@@ -8135,7 +8135,7 @@ module MyErc20-CONTRACT
 
 endmodule
 
-module PlainPrankTest-CONTRACT
+module S2KPlainPrankTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KPlainPrankTestContract
@@ -8408,7 +8408,7 @@ module PlainPrankTest-CONTRACT
 
 endmodule
 
-module Prank-CONTRACT
+module S2KPrank-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KPrankContract
@@ -8465,7 +8465,7 @@ module Prank-CONTRACT
 
 endmodule
 
-module PrankTest-CONTRACT
+module S2KPrankTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KPrankTestContract
@@ -8719,7 +8719,7 @@ module PrankTest-CONTRACT
 
 endmodule
 
-module PreconditionsTest-CONTRACT
+module S2KPreconditionsTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KPreconditionsTestContract
@@ -8931,7 +8931,7 @@ module PreconditionsTest-CONTRACT
 
 endmodule
 
-module RecordLogsTest-CONTRACT
+module S2KRecordLogsTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KRecordLogsTestContract
@@ -9135,7 +9135,7 @@ module RecordLogsTest-CONTRACT
 
 endmodule
 
-module Safe-CONTRACT
+module S2KSafe-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KSafeContract
@@ -9159,7 +9159,7 @@ module Safe-CONTRACT
 
 endmodule
 
-module SafeTest-CONTRACT
+module S2KSafeTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KSafeTestContract
@@ -9372,7 +9372,7 @@ module SafeTest-CONTRACT
 
 endmodule
 
-module Setup2Test-CONTRACT
+module S2KSetup2Test-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KSetup2TestContract
@@ -9594,7 +9594,7 @@ module Setup2Test-CONTRACT
 
 endmodule
 
-module SetUpDeployTest-CONTRACT
+module S2KSetUpDeployTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KSetUpDeployTestContract
@@ -9798,7 +9798,7 @@ module SetUpDeployTest-CONTRACT
 
 endmodule
 
-module SetUpTest-CONTRACT
+module S2KSetUpTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KSetUpTestContract
@@ -10011,7 +10011,7 @@ module SetUpTest-CONTRACT
 
 endmodule
 
-module SignTest-CONTRACT
+module S2KSignTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KSignTestContract
@@ -10211,7 +10211,7 @@ module SignTest-CONTRACT
 
 endmodule
 
-module AssertTest-CONTRACT
+module S2KAssertTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KAssertTestContract
@@ -10484,7 +10484,7 @@ module AssertTest-CONTRACT
 
 endmodule
 
-module SnapshotTest-CONTRACT
+module S2KSnapshotTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KSnapshotTestContract
@@ -10688,7 +10688,7 @@ module SnapshotTest-CONTRACT
 
 endmodule
 
-module StdAssertions-CONTRACT
+module S2KStdAssertions-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KStdAssertionsContract
@@ -10732,7 +10732,7 @@ module StdAssertions-CONTRACT
 
 endmodule
 
-module StdChains-CONTRACT
+module S2KStdChains-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KStdChainsContract
@@ -10773,7 +10773,7 @@ module StdChains-CONTRACT
 
 endmodule
 
-module StdCheats-CONTRACT
+module S2KStdCheats-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KStdCheatsContract
@@ -10799,7 +10799,7 @@ module StdCheats-CONTRACT
 
 endmodule
 
-module StdCheatsSafe-CONTRACT
+module S2KStdCheatsSafe-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KStdCheatsSafeContract
@@ -10820,7 +10820,7 @@ module StdCheatsSafe-CONTRACT
 
 endmodule
 
-module stdError-CONTRACT
+module S2KstdError-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KstdErrorContract
@@ -10908,7 +10908,7 @@ module stdError-CONTRACT
 
 endmodule
 
-module StdInvariant-CONTRACT
+module S2KStdInvariant-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KStdInvariantContract
@@ -11030,7 +11030,7 @@ module StdInvariant-CONTRACT
 
 endmodule
 
-module stdJson-CONTRACT
+module S2KstdJson-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KstdJsonContract
@@ -11044,7 +11044,7 @@ module stdJson-CONTRACT
 
 endmodule
 
-module stdMath-CONTRACT
+module S2KstdMath-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KstdMathContract
@@ -11058,7 +11058,7 @@ module stdMath-CONTRACT
 
 endmodule
 
-module stdStorage-CONTRACT
+module S2KstdStorage-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KstdStorageContract
@@ -11072,7 +11072,7 @@ module stdStorage-CONTRACT
 
 endmodule
 
-module stdStorageSafe-CONTRACT
+module S2KstdStorageSafe-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KstdStorageSafeContract
@@ -11086,7 +11086,7 @@ module stdStorageSafe-CONTRACT
 
 endmodule
 
-module StdStyle-CONTRACT
+module S2KStdStyle-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KStdStyleContract
@@ -11100,7 +11100,7 @@ module StdStyle-CONTRACT
 
 endmodule
 
-module StdUtils-CONTRACT
+module S2KStdUtils-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KStdUtilsContract
@@ -11114,7 +11114,7 @@ module StdUtils-CONTRACT
 
 endmodule
 
-module Store-CONTRACT
+module S2KStore-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KStoreContract
@@ -11135,7 +11135,7 @@ module Store-CONTRACT
 
 endmodule
 
-module StoreTest-CONTRACT
+module S2KStoreTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KStoreTestContract
@@ -11398,7 +11398,7 @@ module StoreTest-CONTRACT
 
 endmodule
 
-module SymbolicStorageTest-CONTRACT
+module S2KSymbolicStorageTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KSymbolicStorageTestContract
@@ -11616,7 +11616,7 @@ module SymbolicStorageTest-CONTRACT
 
 endmodule
 
-module SymbolicStore-CONTRACT
+module S2KSymbolicStore-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KSymbolicStoreContract
@@ -11637,7 +11637,7 @@ module SymbolicStore-CONTRACT
 
 endmodule
 
-module Test-CONTRACT
+module S2KTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KTestContract
@@ -11820,7 +11820,7 @@ module Test-CONTRACT
 
 endmodule
 
-module TestNumber-CONTRACT
+module S2KTestNumber-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KTestNumberContract
@@ -11886,7 +11886,7 @@ module TestNumber-CONTRACT
 
 endmodule
 
-module ToStringTest-CONTRACT
+module S2KToStringTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KToStringTestContract
@@ -12117,7 +12117,7 @@ module ToStringTest-CONTRACT
 
 endmodule
 
-module Token-CONTRACT
+module S2KToken-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KTokenContract
@@ -12186,7 +12186,7 @@ module Token-CONTRACT
 
 endmodule
 
-module BytesTypeTest-CONTRACT
+module S2KBytesTypeTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KBytesTypeTestContract
@@ -12256,7 +12256,7 @@ module BytesTypeTest-CONTRACT
 
 endmodule
 
-module IntTypeTest-CONTRACT
+module S2KIntTypeTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KIntTypeTestContract
@@ -12353,7 +12353,7 @@ module IntTypeTest-CONTRACT
 
 endmodule
 
-module UintTypeTest-CONTRACT
+module S2KUintTypeTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KUintTypeTestContract
@@ -13233,7 +13233,7 @@ module UintTypeTest-CONTRACT
 
 endmodule
 
-module Vm-CONTRACT
+module S2KVm-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KVmContract
@@ -14878,7 +14878,7 @@ module Vm-CONTRACT
 
 endmodule
 
-module VmSafe-CONTRACT
+module S2KVmSafe-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KVmSafeContract
@@ -15854,7 +15854,7 @@ module VmSafe-CONTRACT
 
 endmodule
 
-module console-CONTRACT
+module S2Kconsole-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KconsoleContract
@@ -15868,7 +15868,7 @@ module console-CONTRACT
 
 endmodule
 
-module console2-CONTRACT
+module S2Kconsole2-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2Kconsole2Contract
@@ -15882,7 +15882,7 @@ module console2-CONTRACT
 
 endmodule
 
-module safeconsole-CONTRACT
+module S2Ksafeconsole-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KsafeconsoleContract
@@ -15896,7 +15896,7 @@ module safeconsole-CONTRACT
 
 endmodule
 
-module DSTest-CONTRACT
+module S2KDSTest-CONTRACT
     imports public FOUNDRY
     
     syntax Contract ::= S2KDSTestContract
diff --git a/src/tests/integration/test-data/foundry.k.expected b/src/tests/integration/test-data/foundry.k.expected
index 776a01176..0fa58e722 100644
--- a/src/tests/integration/test-data/foundry.k.expected
+++ b/src/tests/integration/test-data/foundry.k.expected
@@ -2,767 +2,767 @@ requires "contracts.k"
 requires "requires/lemmas.k"
 
 module FOUNDRY-MAIN
-    imports public AccountParamsTest-VERIFICATION
-    imports public AddrTest-VERIFICATION
-    imports public AllowChangesTest-VERIFICATION
-    imports public ValueStore-VERIFICATION
-    imports public AmbiguousTest-VERIFICATION
-    imports public ArithmeticTest-VERIFICATION
-    imports public AssumeTest-VERIFICATION
-    imports public BMCLoopsTest-VERIFICATION
-    imports public CommonBase-VERIFICATION
-    imports public ScriptBase-VERIFICATION
-    imports public TestBase-VERIFICATION
-    imports public BlockParamsTest-VERIFICATION
-    imports public RollTest-VERIFICATION
-    imports public BroadcastTest-VERIFICATION
-    imports public Constants-VERIFICATION
-    imports public Contract-VERIFICATION
-    imports public ContractTest-VERIFICATION
-    imports public ContractBTest-VERIFICATION
-    imports public Counter-VERIFICATION
-    imports public CounterTest-VERIFICATION
-    imports public DynamicTypes-VERIFICATION
-    imports public ExpectEmit-VERIFICATION
-    imports public EmitContractTest-VERIFICATION
-    imports public EnvTest-VERIFICATION
-    imports public Dummy-VERIFICATION
-    imports public ExpectCallTest-VERIFICATION
-    imports public DepthReverter-VERIFICATION
-    imports public ExpectRevertTest-VERIFICATION
-    imports public Reverter-VERIFICATION
-    imports public ReverterWithReturn-VERIFICATION
-    imports public FfiTest-VERIFICATION
-    imports public FilesTest-VERIFICATION
-    imports public ForkTest-VERIFICATION
-    imports public FreshIntTest-VERIFICATION
-    imports public GasTest-VERIFICATION
-    imports public GetCodeTest-VERIFICATION
-    imports public IMulticall3-VERIFICATION
-    imports public InitCodeTest-VERIFICATION
-    imports public InitCodeBranchTest-VERIFICATION
-    imports public KEVMCheats-VERIFICATION
-    imports public KEVMCheatsBase-VERIFICATION
-    imports public LabelTest-VERIFICATION
-    imports public LoopsTest-VERIFICATION
-    imports public MergeTest-VERIFICATION
-    imports public MethodDisambiguateTest-VERIFICATION
-    imports public MockCallTest-VERIFICATION
-    imports public MyIERC20-VERIFICATION
-    imports public MyToken-VERIFICATION
-    imports public NoImport-VERIFICATION
-    imports public OwnerUpOnly-VERIFICATION
-    imports public OwnerUpOnlyTest-VERIFICATION
-    imports public AdditionalToken-VERIFICATION
-    imports public MyErc20-VERIFICATION
-    imports public PlainPrankTest-VERIFICATION
-    imports public Prank-VERIFICATION
-    imports public PrankTest-VERIFICATION
-    imports public PreconditionsTest-VERIFICATION
-    imports public RecordLogsTest-VERIFICATION
-    imports public Safe-VERIFICATION
-    imports public SafeTest-VERIFICATION
-    imports public Setup2Test-VERIFICATION
-    imports public SetUpDeployTest-VERIFICATION
-    imports public SetUpTest-VERIFICATION
-    imports public SignTest-VERIFICATION
-    imports public AssertTest-VERIFICATION
-    imports public SnapshotTest-VERIFICATION
-    imports public StdAssertions-VERIFICATION
-    imports public StdChains-VERIFICATION
-    imports public StdCheats-VERIFICATION
-    imports public StdCheatsSafe-VERIFICATION
-    imports public stdError-VERIFICATION
-    imports public StdInvariant-VERIFICATION
-    imports public stdJson-VERIFICATION
-    imports public stdMath-VERIFICATION
-    imports public stdStorage-VERIFICATION
-    imports public stdStorageSafe-VERIFICATION
-    imports public StdStyle-VERIFICATION
-    imports public StdUtils-VERIFICATION
-    imports public Store-VERIFICATION
-    imports public StoreTest-VERIFICATION
-    imports public SymbolicStorageTest-VERIFICATION
-    imports public SymbolicStore-VERIFICATION
-    imports public Test-VERIFICATION
-    imports public TestNumber-VERIFICATION
-    imports public ToStringTest-VERIFICATION
-    imports public Token-VERIFICATION
-    imports public BytesTypeTest-VERIFICATION
-    imports public IntTypeTest-VERIFICATION
-    imports public UintTypeTest-VERIFICATION
-    imports public Vm-VERIFICATION
-    imports public VmSafe-VERIFICATION
-    imports public console-VERIFICATION
-    imports public console2-VERIFICATION
-    imports public safeconsole-VERIFICATION
-    imports public DSTest-VERIFICATION
+    imports public S2KAccountParamsTest-VERIFICATION
+    imports public S2KAddrTest-VERIFICATION
+    imports public S2KAllowChangesTest-VERIFICATION
+    imports public S2KValueStore-VERIFICATION
+    imports public S2KAmbiguousTest-VERIFICATION
+    imports public S2KArithmeticTest-VERIFICATION
+    imports public S2KAssumeTest-VERIFICATION
+    imports public S2KBMCLoopsTest-VERIFICATION
+    imports public S2KCommonBase-VERIFICATION
+    imports public S2KScriptBase-VERIFICATION
+    imports public S2KTestBase-VERIFICATION
+    imports public S2KBlockParamsTest-VERIFICATION
+    imports public S2KRollTest-VERIFICATION
+    imports public S2KBroadcastTest-VERIFICATION
+    imports public S2KConstants-VERIFICATION
+    imports public S2KContract-VERIFICATION
+    imports public S2KContractTest-VERIFICATION
+    imports public S2KContractBTest-VERIFICATION
+    imports public S2KCounter-VERIFICATION
+    imports public S2KCounterTest-VERIFICATION
+    imports public S2KDynamicTypes-VERIFICATION
+    imports public S2KExpectEmit-VERIFICATION
+    imports public S2KEmitContractTest-VERIFICATION
+    imports public S2KEnvTest-VERIFICATION
+    imports public S2KDummy-VERIFICATION
+    imports public S2KExpectCallTest-VERIFICATION
+    imports public S2KDepthReverter-VERIFICATION
+    imports public S2KExpectRevertTest-VERIFICATION
+    imports public S2KReverter-VERIFICATION
+    imports public S2KReverterWithReturn-VERIFICATION
+    imports public S2KFfiTest-VERIFICATION
+    imports public S2KFilesTest-VERIFICATION
+    imports public S2KForkTest-VERIFICATION
+    imports public S2KFreshIntTest-VERIFICATION
+    imports public S2KGasTest-VERIFICATION
+    imports public S2KGetCodeTest-VERIFICATION
+    imports public S2KIMulticall3-VERIFICATION
+    imports public S2KInitCodeTest-VERIFICATION
+    imports public S2KInitCodeBranchTest-VERIFICATION
+    imports public S2KKEVMCheats-VERIFICATION
+    imports public S2KKEVMCheatsBase-VERIFICATION
+    imports public S2KLabelTest-VERIFICATION
+    imports public S2KLoopsTest-VERIFICATION
+    imports public S2KMergeTest-VERIFICATION
+    imports public S2KMethodDisambiguateTest-VERIFICATION
+    imports public S2KMockCallTest-VERIFICATION
+    imports public S2KMyIERC20-VERIFICATION
+    imports public S2KMyToken-VERIFICATION
+    imports public S2KNoImport-VERIFICATION
+    imports public S2KOwnerUpOnly-VERIFICATION
+    imports public S2KOwnerUpOnlyTest-VERIFICATION
+    imports public S2KAdditionalToken-VERIFICATION
+    imports public S2KMyErc20-VERIFICATION
+    imports public S2KPlainPrankTest-VERIFICATION
+    imports public S2KPrank-VERIFICATION
+    imports public S2KPrankTest-VERIFICATION
+    imports public S2KPreconditionsTest-VERIFICATION
+    imports public S2KRecordLogsTest-VERIFICATION
+    imports public S2KSafe-VERIFICATION
+    imports public S2KSafeTest-VERIFICATION
+    imports public S2KSetup2Test-VERIFICATION
+    imports public S2KSetUpDeployTest-VERIFICATION
+    imports public S2KSetUpTest-VERIFICATION
+    imports public S2KSignTest-VERIFICATION
+    imports public S2KAssertTest-VERIFICATION
+    imports public S2KSnapshotTest-VERIFICATION
+    imports public S2KStdAssertions-VERIFICATION
+    imports public S2KStdChains-VERIFICATION
+    imports public S2KStdCheats-VERIFICATION
+    imports public S2KStdCheatsSafe-VERIFICATION
+    imports public S2KstdError-VERIFICATION
+    imports public S2KStdInvariant-VERIFICATION
+    imports public S2KstdJson-VERIFICATION
+    imports public S2KstdMath-VERIFICATION
+    imports public S2KstdStorage-VERIFICATION
+    imports public S2KstdStorageSafe-VERIFICATION
+    imports public S2KStdStyle-VERIFICATION
+    imports public S2KStdUtils-VERIFICATION
+    imports public S2KStore-VERIFICATION
+    imports public S2KStoreTest-VERIFICATION
+    imports public S2KSymbolicStorageTest-VERIFICATION
+    imports public S2KSymbolicStore-VERIFICATION
+    imports public S2KTest-VERIFICATION
+    imports public S2KTestNumber-VERIFICATION
+    imports public S2KToStringTest-VERIFICATION
+    imports public S2KToken-VERIFICATION
+    imports public S2KBytesTypeTest-VERIFICATION
+    imports public S2KIntTypeTest-VERIFICATION
+    imports public S2KUintTypeTest-VERIFICATION
+    imports public S2KVm-VERIFICATION
+    imports public S2KVmSafe-VERIFICATION
+    imports public S2Kconsole-VERIFICATION
+    imports public S2Kconsole2-VERIFICATION
+    imports public S2Ksafeconsole-VERIFICATION
+    imports public S2KDSTest-VERIFICATION
     
     
 
 endmodule
 
-module AccountParamsTest-VERIFICATION
-    imports public AccountParamsTest-CONTRACT
+module S2KAccountParamsTest-VERIFICATION
+    imports public S2KAccountParamsTest-CONTRACT
     
     
 
 endmodule
 
-module AddrTest-VERIFICATION
-    imports public AddrTest-CONTRACT
+module S2KAddrTest-VERIFICATION
+    imports public S2KAddrTest-CONTRACT
     
     
 
 endmodule
 
-module AllowChangesTest-VERIFICATION
-    imports public AllowChangesTest-CONTRACT
+module S2KAllowChangesTest-VERIFICATION
+    imports public S2KAllowChangesTest-CONTRACT
     
     
 
 endmodule
 
-module ValueStore-VERIFICATION
-    imports public ValueStore-CONTRACT
+module S2KValueStore-VERIFICATION
+    imports public S2KValueStore-CONTRACT
     
     
 
 endmodule
 
-module AmbiguousTest-VERIFICATION
-    imports public AmbiguousTest-CONTRACT
+module S2KAmbiguousTest-VERIFICATION
+    imports public S2KAmbiguousTest-CONTRACT
     
     
 
 endmodule
 
-module ArithmeticTest-VERIFICATION
-    imports public ArithmeticTest-CONTRACT
+module S2KArithmeticTest-VERIFICATION
+    imports public S2KArithmeticTest-CONTRACT
     
     
 
 endmodule
 
-module AssumeTest-VERIFICATION
-    imports public AssumeTest-CONTRACT
+module S2KAssumeTest-VERIFICATION
+    imports public S2KAssumeTest-CONTRACT
     
     
 
 endmodule
 
-module BMCLoopsTest-VERIFICATION
-    imports public BMCLoopsTest-CONTRACT
+module S2KBMCLoopsTest-VERIFICATION
+    imports public S2KBMCLoopsTest-CONTRACT
     
     
 
 endmodule
 
-module CommonBase-VERIFICATION
-    imports public CommonBase-CONTRACT
+module S2KCommonBase-VERIFICATION
+    imports public S2KCommonBase-CONTRACT
     
     
 
 endmodule
 
-module ScriptBase-VERIFICATION
-    imports public ScriptBase-CONTRACT
+module S2KScriptBase-VERIFICATION
+    imports public S2KScriptBase-CONTRACT
     
     
 
 endmodule
 
-module TestBase-VERIFICATION
-    imports public TestBase-CONTRACT
+module S2KTestBase-VERIFICATION
+    imports public S2KTestBase-CONTRACT
     
     
 
 endmodule
 
-module BlockParamsTest-VERIFICATION
-    imports public BlockParamsTest-CONTRACT
+module S2KBlockParamsTest-VERIFICATION
+    imports public S2KBlockParamsTest-CONTRACT
     
     
 
 endmodule
 
-module RollTest-VERIFICATION
-    imports public RollTest-CONTRACT
+module S2KRollTest-VERIFICATION
+    imports public S2KRollTest-CONTRACT
     
     
 
 endmodule
 
-module BroadcastTest-VERIFICATION
-    imports public BroadcastTest-CONTRACT
+module S2KBroadcastTest-VERIFICATION
+    imports public S2KBroadcastTest-CONTRACT
     
     
 
 endmodule
 
-module Constants-VERIFICATION
-    imports public Constants-CONTRACT
+module S2KConstants-VERIFICATION
+    imports public S2KConstants-CONTRACT
     
     
 
 endmodule
 
-module Contract-VERIFICATION
-    imports public Contract-CONTRACT
+module S2KContract-VERIFICATION
+    imports public S2KContract-CONTRACT
     
     
 
 endmodule
 
-module ContractTest-VERIFICATION
-    imports public ContractTest-CONTRACT
+module S2KContractTest-VERIFICATION
+    imports public S2KContractTest-CONTRACT
     
     
 
 endmodule
 
-module ContractBTest-VERIFICATION
-    imports public ContractBTest-CONTRACT
+module S2KContractBTest-VERIFICATION
+    imports public S2KContractBTest-CONTRACT
     
     
 
 endmodule
 
-module Counter-VERIFICATION
-    imports public Counter-CONTRACT
+module S2KCounter-VERIFICATION
+    imports public S2KCounter-CONTRACT
     
     
 
 endmodule
 
-module CounterTest-VERIFICATION
-    imports public CounterTest-CONTRACT
+module S2KCounterTest-VERIFICATION
+    imports public S2KCounterTest-CONTRACT
     
     
 
 endmodule
 
-module DynamicTypes-VERIFICATION
-    imports public DynamicTypes-CONTRACT
+module S2KDynamicTypes-VERIFICATION
+    imports public S2KDynamicTypes-CONTRACT
     
     
 
 endmodule
 
-module ExpectEmit-VERIFICATION
-    imports public ExpectEmit-CONTRACT
+module S2KExpectEmit-VERIFICATION
+    imports public S2KExpectEmit-CONTRACT
     
     
 
 endmodule
 
-module EmitContractTest-VERIFICATION
-    imports public EmitContractTest-CONTRACT
+module S2KEmitContractTest-VERIFICATION
+    imports public S2KEmitContractTest-CONTRACT
     
     
 
 endmodule
 
-module EnvTest-VERIFICATION
-    imports public EnvTest-CONTRACT
+module S2KEnvTest-VERIFICATION
+    imports public S2KEnvTest-CONTRACT
     
     
 
 endmodule
 
-module Dummy-VERIFICATION
-    imports public Dummy-CONTRACT
+module S2KDummy-VERIFICATION
+    imports public S2KDummy-CONTRACT
     
     
 
 endmodule
 
-module ExpectCallTest-VERIFICATION
-    imports public ExpectCallTest-CONTRACT
+module S2KExpectCallTest-VERIFICATION
+    imports public S2KExpectCallTest-CONTRACT
     
     
 
 endmodule
 
-module DepthReverter-VERIFICATION
-    imports public DepthReverter-CONTRACT
+module S2KDepthReverter-VERIFICATION
+    imports public S2KDepthReverter-CONTRACT
     
     
 
 endmodule
 
-module ExpectRevertTest-VERIFICATION
-    imports public ExpectRevertTest-CONTRACT
+module S2KExpectRevertTest-VERIFICATION
+    imports public S2KExpectRevertTest-CONTRACT
     
     
 
 endmodule
 
-module Reverter-VERIFICATION
-    imports public Reverter-CONTRACT
+module S2KReverter-VERIFICATION
+    imports public S2KReverter-CONTRACT
     
     
 
 endmodule
 
-module ReverterWithReturn-VERIFICATION
-    imports public ReverterWithReturn-CONTRACT
+module S2KReverterWithReturn-VERIFICATION
+    imports public S2KReverterWithReturn-CONTRACT
     
     
 
 endmodule
 
-module FfiTest-VERIFICATION
-    imports public FfiTest-CONTRACT
+module S2KFfiTest-VERIFICATION
+    imports public S2KFfiTest-CONTRACT
     
     
 
 endmodule
 
-module FilesTest-VERIFICATION
-    imports public FilesTest-CONTRACT
+module S2KFilesTest-VERIFICATION
+    imports public S2KFilesTest-CONTRACT
     
     
 
 endmodule
 
-module ForkTest-VERIFICATION
-    imports public ForkTest-CONTRACT
+module S2KForkTest-VERIFICATION
+    imports public S2KForkTest-CONTRACT
     
     
 
 endmodule
 
-module FreshIntTest-VERIFICATION
-    imports public FreshIntTest-CONTRACT
+module S2KFreshIntTest-VERIFICATION
+    imports public S2KFreshIntTest-CONTRACT
     
     
 
 endmodule
 
-module GasTest-VERIFICATION
-    imports public GasTest-CONTRACT
+module S2KGasTest-VERIFICATION
+    imports public S2KGasTest-CONTRACT
     
     
 
 endmodule
 
-module GetCodeTest-VERIFICATION
-    imports public GetCodeTest-CONTRACT
+module S2KGetCodeTest-VERIFICATION
+    imports public S2KGetCodeTest-CONTRACT
     
     
 
 endmodule
 
-module IMulticall3-VERIFICATION
-    imports public IMulticall3-CONTRACT
+module S2KIMulticall3-VERIFICATION
+    imports public S2KIMulticall3-CONTRACT
     
     
 
 endmodule
 
-module InitCodeTest-VERIFICATION
-    imports public InitCodeTest-CONTRACT
+module S2KInitCodeTest-VERIFICATION
+    imports public S2KInitCodeTest-CONTRACT
     
     
 
 endmodule
 
-module InitCodeBranchTest-VERIFICATION
-    imports public InitCodeBranchTest-CONTRACT
+module S2KInitCodeBranchTest-VERIFICATION
+    imports public S2KInitCodeBranchTest-CONTRACT
     
     
 
 endmodule
 
-module KEVMCheats-VERIFICATION
-    imports public KEVMCheats-CONTRACT
+module S2KKEVMCheats-VERIFICATION
+    imports public S2KKEVMCheats-CONTRACT
     
     
 
 endmodule
 
-module KEVMCheatsBase-VERIFICATION
-    imports public KEVMCheatsBase-CONTRACT
+module S2KKEVMCheatsBase-VERIFICATION
+    imports public S2KKEVMCheatsBase-CONTRACT
     
     
 
 endmodule
 
-module LabelTest-VERIFICATION
-    imports public LabelTest-CONTRACT
+module S2KLabelTest-VERIFICATION
+    imports public S2KLabelTest-CONTRACT
     
     
 
 endmodule
 
-module LoopsTest-VERIFICATION
-    imports public LoopsTest-CONTRACT
+module S2KLoopsTest-VERIFICATION
+    imports public S2KLoopsTest-CONTRACT
     imports public SUM-TO-N-INVARIANT
     
     
 
 endmodule
 
-module MergeTest-VERIFICATION
-    imports public MergeTest-CONTRACT
+module S2KMergeTest-VERIFICATION
+    imports public S2KMergeTest-CONTRACT
     
     
 
 endmodule
 
-module MethodDisambiguateTest-VERIFICATION
-    imports public MethodDisambiguateTest-CONTRACT
+module S2KMethodDisambiguateTest-VERIFICATION
+    imports public S2KMethodDisambiguateTest-CONTRACT
     
     
 
 endmodule
 
-module MockCallTest-VERIFICATION
-    imports public MockCallTest-CONTRACT
+module S2KMockCallTest-VERIFICATION
+    imports public S2KMockCallTest-CONTRACT
     
     
 
 endmodule
 
-module MyIERC20-VERIFICATION
-    imports public MyIERC20-CONTRACT
+module S2KMyIERC20-VERIFICATION
+    imports public S2KMyIERC20-CONTRACT
     
     
 
 endmodule
 
-module MyToken-VERIFICATION
-    imports public MyToken-CONTRACT
+module S2KMyToken-VERIFICATION
+    imports public S2KMyToken-CONTRACT
     
     
 
 endmodule
 
-module NoImport-VERIFICATION
-    imports public NoImport-CONTRACT
+module S2KNoImport-VERIFICATION
+    imports public S2KNoImport-CONTRACT
     
     
 
 endmodule
 
-module OwnerUpOnly-VERIFICATION
-    imports public OwnerUpOnly-CONTRACT
+module S2KOwnerUpOnly-VERIFICATION
+    imports public S2KOwnerUpOnly-CONTRACT
     
     
 
 endmodule
 
-module OwnerUpOnlyTest-VERIFICATION
-    imports public OwnerUpOnlyTest-CONTRACT
+module S2KOwnerUpOnlyTest-VERIFICATION
+    imports public S2KOwnerUpOnlyTest-CONTRACT
     
     
 
 endmodule
 
-module AdditionalToken-VERIFICATION
-    imports public AdditionalToken-CONTRACT
+module S2KAdditionalToken-VERIFICATION
+    imports public S2KAdditionalToken-CONTRACT
     
     
 
 endmodule
 
-module MyErc20-VERIFICATION
-    imports public MyErc20-CONTRACT
+module S2KMyErc20-VERIFICATION
+    imports public S2KMyErc20-CONTRACT
     
     
 
 endmodule
 
-module PlainPrankTest-VERIFICATION
-    imports public PlainPrankTest-CONTRACT
+module S2KPlainPrankTest-VERIFICATION
+    imports public S2KPlainPrankTest-CONTRACT
     
     
 
 endmodule
 
-module Prank-VERIFICATION
-    imports public Prank-CONTRACT
+module S2KPrank-VERIFICATION
+    imports public S2KPrank-CONTRACT
     
     
 
 endmodule
 
-module PrankTest-VERIFICATION
-    imports public PrankTest-CONTRACT
+module S2KPrankTest-VERIFICATION
+    imports public S2KPrankTest-CONTRACT
     
     
 
 endmodule
 
-module PreconditionsTest-VERIFICATION
-    imports public PreconditionsTest-CONTRACT
+module S2KPreconditionsTest-VERIFICATION
+    imports public S2KPreconditionsTest-CONTRACT
     
     
 
 endmodule
 
-module RecordLogsTest-VERIFICATION
-    imports public RecordLogsTest-CONTRACT
+module S2KRecordLogsTest-VERIFICATION
+    imports public S2KRecordLogsTest-CONTRACT
     
     
 
 endmodule
 
-module Safe-VERIFICATION
-    imports public Safe-CONTRACT
+module S2KSafe-VERIFICATION
+    imports public S2KSafe-CONTRACT
     
     
 
 endmodule
 
-module SafeTest-VERIFICATION
-    imports public SafeTest-CONTRACT
+module S2KSafeTest-VERIFICATION
+    imports public S2KSafeTest-CONTRACT
     
     
 
 endmodule
 
-module Setup2Test-VERIFICATION
-    imports public Setup2Test-CONTRACT
+module S2KSetup2Test-VERIFICATION
+    imports public S2KSetup2Test-CONTRACT
     
     
 
 endmodule
 
-module SetUpDeployTest-VERIFICATION
-    imports public SetUpDeployTest-CONTRACT
+module S2KSetUpDeployTest-VERIFICATION
+    imports public S2KSetUpDeployTest-CONTRACT
     
     
 
 endmodule
 
-module SetUpTest-VERIFICATION
-    imports public SetUpTest-CONTRACT
+module S2KSetUpTest-VERIFICATION
+    imports public S2KSetUpTest-CONTRACT
     
     
 
 endmodule
 
-module SignTest-VERIFICATION
-    imports public SignTest-CONTRACT
+module S2KSignTest-VERIFICATION
+    imports public S2KSignTest-CONTRACT
     
     
 
 endmodule
 
-module AssertTest-VERIFICATION
-    imports public AssertTest-CONTRACT
+module S2KAssertTest-VERIFICATION
+    imports public S2KAssertTest-CONTRACT
     
     
 
 endmodule
 
-module SnapshotTest-VERIFICATION
-    imports public SnapshotTest-CONTRACT
+module S2KSnapshotTest-VERIFICATION
+    imports public S2KSnapshotTest-CONTRACT
     
     
 
 endmodule
 
-module StdAssertions-VERIFICATION
-    imports public StdAssertions-CONTRACT
+module S2KStdAssertions-VERIFICATION
+    imports public S2KStdAssertions-CONTRACT
     
     
 
 endmodule
 
-module StdChains-VERIFICATION
-    imports public StdChains-CONTRACT
+module S2KStdChains-VERIFICATION
+    imports public S2KStdChains-CONTRACT
     
     
 
 endmodule
 
-module StdCheats-VERIFICATION
-    imports public StdCheats-CONTRACT
+module S2KStdCheats-VERIFICATION
+    imports public S2KStdCheats-CONTRACT
     
     
 
 endmodule
 
-module StdCheatsSafe-VERIFICATION
-    imports public StdCheatsSafe-CONTRACT
+module S2KStdCheatsSafe-VERIFICATION
+    imports public S2KStdCheatsSafe-CONTRACT
     
     
 
 endmodule
 
-module stdError-VERIFICATION
-    imports public stdError-CONTRACT
+module S2KstdError-VERIFICATION
+    imports public S2KstdError-CONTRACT
     
     
 
 endmodule
 
-module StdInvariant-VERIFICATION
-    imports public StdInvariant-CONTRACT
+module S2KStdInvariant-VERIFICATION
+    imports public S2KStdInvariant-CONTRACT
     
     
 
 endmodule
 
-module stdJson-VERIFICATION
-    imports public stdJson-CONTRACT
+module S2KstdJson-VERIFICATION
+    imports public S2KstdJson-CONTRACT
     
     
 
 endmodule
 
-module stdMath-VERIFICATION
-    imports public stdMath-CONTRACT
+module S2KstdMath-VERIFICATION
+    imports public S2KstdMath-CONTRACT
     
     
 
 endmodule
 
-module stdStorage-VERIFICATION
-    imports public stdStorage-CONTRACT
+module S2KstdStorage-VERIFICATION
+    imports public S2KstdStorage-CONTRACT
     
     
 
 endmodule
 
-module stdStorageSafe-VERIFICATION
-    imports public stdStorageSafe-CONTRACT
+module S2KstdStorageSafe-VERIFICATION
+    imports public S2KstdStorageSafe-CONTRACT
     
     
 
 endmodule
 
-module StdStyle-VERIFICATION
-    imports public StdStyle-CONTRACT
+module S2KStdStyle-VERIFICATION
+    imports public S2KStdStyle-CONTRACT
     
     
 
 endmodule
 
-module StdUtils-VERIFICATION
-    imports public StdUtils-CONTRACT
+module S2KStdUtils-VERIFICATION
+    imports public S2KStdUtils-CONTRACT
     
     
 
 endmodule
 
-module Store-VERIFICATION
-    imports public Store-CONTRACT
+module S2KStore-VERIFICATION
+    imports public S2KStore-CONTRACT
     
     
 
 endmodule
 
-module StoreTest-VERIFICATION
-    imports public StoreTest-CONTRACT
+module S2KStoreTest-VERIFICATION
+    imports public S2KStoreTest-CONTRACT
     
     
 
 endmodule
 
-module SymbolicStorageTest-VERIFICATION
-    imports public SymbolicStorageTest-CONTRACT
+module S2KSymbolicStorageTest-VERIFICATION
+    imports public S2KSymbolicStorageTest-CONTRACT
     
     
 
 endmodule
 
-module SymbolicStore-VERIFICATION
-    imports public SymbolicStore-CONTRACT
+module S2KSymbolicStore-VERIFICATION
+    imports public S2KSymbolicStore-CONTRACT
     
     
 
 endmodule
 
-module Test-VERIFICATION
-    imports public Test-CONTRACT
+module S2KTest-VERIFICATION
+    imports public S2KTest-CONTRACT
     
     
 
 endmodule
 
-module TestNumber-VERIFICATION
-    imports public TestNumber-CONTRACT
+module S2KTestNumber-VERIFICATION
+    imports public S2KTestNumber-CONTRACT
     
     
 
 endmodule
 
-module ToStringTest-VERIFICATION
-    imports public ToStringTest-CONTRACT
+module S2KToStringTest-VERIFICATION
+    imports public S2KToStringTest-CONTRACT
     
     
 
 endmodule
 
-module Token-VERIFICATION
-    imports public Token-CONTRACT
+module S2KToken-VERIFICATION
+    imports public S2KToken-CONTRACT
     
     
 
 endmodule
 
-module BytesTypeTest-VERIFICATION
-    imports public BytesTypeTest-CONTRACT
+module S2KBytesTypeTest-VERIFICATION
+    imports public S2KBytesTypeTest-CONTRACT
     
     
 
 endmodule
 
-module IntTypeTest-VERIFICATION
-    imports public IntTypeTest-CONTRACT
+module S2KIntTypeTest-VERIFICATION
+    imports public S2KIntTypeTest-CONTRACT
     
     
 
 endmodule
 
-module UintTypeTest-VERIFICATION
-    imports public UintTypeTest-CONTRACT
+module S2KUintTypeTest-VERIFICATION
+    imports public S2KUintTypeTest-CONTRACT
     
     
 
 endmodule
 
-module Vm-VERIFICATION
-    imports public Vm-CONTRACT
+module S2KVm-VERIFICATION
+    imports public S2KVm-CONTRACT
     
     
 
 endmodule
 
-module VmSafe-VERIFICATION
-    imports public VmSafe-CONTRACT
+module S2KVmSafe-VERIFICATION
+    imports public S2KVmSafe-CONTRACT
     
     
 
 endmodule
 
-module console-VERIFICATION
-    imports public console-CONTRACT
+module S2Kconsole-VERIFICATION
+    imports public S2Kconsole-CONTRACT
     
     
 
 endmodule
 
-module console2-VERIFICATION
-    imports public console2-CONTRACT
+module S2Kconsole2-VERIFICATION
+    imports public S2Kconsole2-CONTRACT
     
     
 
 endmodule
 
-module safeconsole-VERIFICATION
-    imports public safeconsole-CONTRACT
+module S2Ksafeconsole-VERIFICATION
+    imports public S2Ksafeconsole-CONTRACT
     
     
 
 endmodule
 
-module DSTest-VERIFICATION
-    imports public DSTest-CONTRACT
+module S2KDSTest-VERIFICATION
+    imports public S2KDSTest-CONTRACT
     
     
 
diff --git a/src/tests/integration/test-data/lemmas.k b/src/tests/integration/test-data/lemmas.k
index 01653802f..305116584 100644
--- a/src/tests/integration/test-data/lemmas.k
+++ b/src/tests/integration/test-data/lemmas.k
@@ -2,7 +2,7 @@ requires "../contracts.k"
 
 module SUM-TO-N-INVARIANT
 
-  imports LoopsTest-CONTRACT
+  imports S2KLoopsTest-CONTRACT
 
   rule N xorInt maxUInt256 => maxUInt256 -Int N 
   requires #rangeUInt(256, N)