diff --git a/src/komet/proof.py b/src/komet/proof.py
index 7b1a581..5469948 100644
--- 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
index a990b1f..3e6a667 100644
--- 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'))