Common pitfall
What is an infinite loop of the prover?
For instance, consider applying the rule:
on the following goal
We will obtain successively the following goals:
The kernel of the prover then produces the following messageskrt: sequence memory short
The messages krt: sequence memory short are generated by the kernel when it dynamically claims additional memory.
This example is simple. Infinite loops may be caused by combination of rule applications and be more difficult to detect a priori.
Last updated
Was this helpful?