#170 Provers end in an infinite loop
After changing the attached project, about 20 instances of the process "krt" are started and remain running, even when the project is rebuilt.
The last change was something on the invariant inv8, but the problem occured in other occasions two.
I'm running the version from cvs (approximately today, 11:30) under java 1.6, 64bit, linux, ubuntu.
Because of compatibility problems, I renamed the directory
"os/linux/x86" of
com.b4free.rodin.linux in
"os/linux/x86_64".
Here the relevant parts of the logfile:
!ENTRY org.eclipse.osgi 2 1 2007-11-19 13:06:44.323
!MESSAGE NLS unused message: symtab_cannotCreateAbstractConstant in: org.eventb.internal.core.sc.messages
!ENTRY org.eclipse.osgi 2 1 2007-11-19 13:06:44.323
!MESSAGE NLS unused message: symtab_cannotCreateAbstractCarrierSet in: org.eventb.internal.core.sc.messages
project
Logged In: YES
user_id=1041912
Originator: NO
Yes, I've reproduced this bug.
The problem is that when a B4free prover reaches a time-out, the Rodin platform goes to the next proof, but doesn't stop the underlying prover.
I'm planning to fix thisi bug soon. In the meantime, you can kill directly the krt processes with "killall -2 krt".
Logged In: YES
user_id=1041912
Originator: NO
This has been fixed in CVS.