Skip to content
This repository was archived by the owner on Apr 25, 2024. It is now read-only.

Commit b6f6f4e

Browse files
committed
Fix injected module name in APRProver
Ensure that the first character is a letter.
1 parent b62bc09 commit b6f6f4e

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/pyk/proof/reachability.py

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -665,7 +665,7 @@ def _inject_module(module_name: str, import_name: str, sentences: list[KRuleLike
665665
dependencies_as_rules.append(apr_subproof.as_rule(priority=20))
666666
circularity_rule = proof.as_rule(priority=20)
667667

668-
module_name = re.sub(r'[_%().:,]+', '-', self.proof.id.upper())
668+
module_name = 'M-' + re.sub(r'[_%().:,]+', '-', self.proof.id.upper())
669669
self.dependencies_module_name = module_name + '-DEPENDS-MODULE'
670670
self.circularities_module_name = module_name + '-CIRCULARITIES-MODULE'
671671
_inject_module(self.dependencies_module_name, self.main_module_name, dependencies_as_rules)

0 commit comments

Comments
 (0)