Enable booster

runtimeverification · Sep 16, 2024 · 9015c58 · 9015c58
1 parent 7c2d233
commit 9015c58
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/src/komet/proof.py b/src/komet/proof.py
@@ -8,7 +8,7 @@
 from pyk.kcfg.semantics import DefaultSemantics
 from pyk.proof import APRProof, APRProver
 
-from .utils import symbolic_definition
+from .utils import symbolic_definition, library_definition
 
 if TYPE_CHECKING:
     from collections.abc import Iterator
@@ -23,6 +23,7 @@ def _explore_context(id: str, bug_report: BugReport | None) -> Iterator[KCFGExpl
     with cterm_symbolic(
         definition=symbolic_definition.kdefinition,
         definition_dir=symbolic_definition.path,
+        llvm_definition_dir=library_definition.path,
         id=id if bug_report else None,
         bug_report=bug_report,
     ) as cts:

diff --git a/src/komet/utils.py b/src/komet/utils.py
@@ -64,4 +64,5 @@ def krun_with_kast(self, pgm: KInner, sort: KSort | None = None, **kwargs: Any)
 
 
 concrete_definition = SorobanDefinition(kdist.get('soroban-semantics.llvm'))
+library_definition = SorobanDefinition(kdist.get('soroban-semantics.llvm-library'))
 symbolic_definition = SorobanDefinition(kdist.get('soroban-semantics.haskell'))
Original file line number	Diff line number	Diff line change
Expand Up		@@ -64,4 +64,5 @@ def krun_with_kast(self, pgm: KInner, sort: KSort \| None = None, **kwargs: Any)


		concrete_definition = SorobanDefinition(kdist.get('soroban-semantics.llvm'))
		library_definition = SorobanDefinition(kdist.get('soroban-semantics.llvm-library'))
		symbolic_definition = SorobanDefinition(kdist.get('soroban-semantics.haskell'))