RUNNING APROVE
filename: CookSeeZuleger-TACAS2013-Fig7b_true-termination.c.pass1.llvm
Graph finished, checking  consistency
Graph finished, checked consistency, took 0.0s
Aborted 1599070382Exec. 5, IRSwTFormatTransformer with some error. Reason: java.lang.RuntimeException: IRSwTFormatTranslator must not transform a single rule into multiple rules in certified mode.
            aprove.Framework.IRSwT.IRSwTFormatTransformer.transform(IRSwTFormatTransformer.java:652)
            aprove.Framework.IRSwT.IRSwTFormatTransformer.process(IRSwTFormatTransformer.java:843)
            aprove.Strategies.ExecutableStrategies.Executor.execute(Executor.java:326)
            aprove.Strategies.ExecutableStrategies.Executor$Runner.wrappedRun(Executor.java:377)
            aprove.Strategies.Abortions.PooledJob.run(PooledJob.java:99)
            aprove.Strategies.Util.PrioritizableThreadPool$Worker.run(PrioritizableThreadPool.java:274)
            java.lang.Thread.run(Thread.java:748)
java.lang.RuntimeException: IRSwTFormatTranslator must not transform a single rule into multiple rules in certified mode
	at aprove.Framework.IRSwT.IRSwTFormatTransformer.transform(IRSwTFormatTransformer.java:652)
	at aprove.Framework.IRSwT.IRSwTFormatTransformer.process(IRSwTFormatTransformer.java:843)
	at aprove.Strategies.ExecutableStrategies.Executor.execute(Executor.java:326)
	at aprove.Strategies.ExecutableStrategies.Executor$Runner.wrappedRun(Executor.java:377)
	at aprove.Strategies.Abortions.PooledJob.run(PooledJob.java:99)
	at aprove.Strategies.Util.PrioritizableThreadPool$Worker.run(PrioritizableThreadPool.java:274)
	at java.lang.Thread.run(Thread.java:748)

real	0m5.795s
user	0m14.777s
sys	0m0.569s