Question about BuchiAutomizer

[WHITE000CHOCOLATE]

I have installed Ultimate 0.2.3 from dev branch in my Windows 10 system and I've loaded the setting located at trunk/examples/settings/default/automizer/svcomp-Termination-64bit-Automizer_Default.epf. I use the BuchiAutomizerBpl.xml to verify the termination of the following program:

procedure main() returns ()
{
    var x, y : int;
    havoc x, y;
    assume (x < 0 || y < 0);
    while (x >= 0) {
        x := x + y;
    }
}

However, I found it impossible to prove the termination. But in the online tool (https://www.ultimate-pa.org/?ui=int&tool=buechi_automizer#), it successfully proved the termination. I wonder if there is something wrong in my settings, or I carelessly destroyed something during my coding? Thanks very much.

[schuessf]

What exactly do you mean by "impossible to prove the termination"? Does ULTIMATE crash or not terminate on this program? I just checked it myself, and here everything looks fine.

[WHITE000CHOCOLATE]

I mean ULTIMATE does not terminate on this program, the termination argument is null. Maybe should the program be decomposed into two lassos? (consider the 'assume A or B' referring to two cases) I found that my ULTIMATE analyze it as one whole lasso, so the condition 'x<0' and 'y<0' should both implies the supporting invariant, and SMT solver returns UNSAT.

[schuessf]

I get the following results with your settings and toolchain (after a few seconds):

- StatisticsResult: Constructed decomposition of program
  Your program was decomposed into 1 terminating modules (0 trivial, 1 deterministic, 0 nondeterministic). One deterministic module has affine ranking function 2 * x + 1 and consists of 4 locations. 

- TerminationAnalysisResult: Termination proven
  Buchi Automizer proved that your program is terminating

Could you please send the log file that you are getting?

[WHITE000CHOCOLATE]

Oh I think I find the problem... The proving was failed for the first time, but after concatenating loop to stem and trying again, the program can be proved terminating. Sorry to bother you and thank you very much!!! (^__^)