kompile and ktest kompile differently

[laurayuwen]

Very strange problem:

yuwen2@yuwen2-HP-Z220-CMT-Workstation:~/k/k-distribution/tutorial/1_k/5_types/lesson_1$ ktest tests/config.xml
Running ['/home/yuwen2/k/k-distribution/target/release/k/bin/kompile' '/home/yuwen2/k/k-distribution/tutorial/1_k/5_types/lesson_1/imp.k']
Done with ['/home/yuwen2/k/k-distribution/target/release/k/bin/kompile' '/home/yuwen2/k/k-distribution/tutorial/1_k/5_types/lesson_1/imp.k']

After I run the above ktest, krun right after that produced correct result; however, if I kompile the definition directly, krun produced a different result.

yuwen2@yuwen2-HP-Z220-CMT-Workstation:~/k/k-distribution/tutorial/1_k/5_types/lesson_1$ krun ../../4_imp++/lesson_1/tests/locals.imp --parser 'kast --sort Stmts'
<T> <k> stmt </k> <tenv> x |-> int </tenv> </T>
yuwen2@yuwen2-HP-Z220-CMT-Workstation:~/k/k-distribution/tutorial/1_k/5_types/lesson_1$ kompile imp.k
yuwen2@yuwen2-HP-Z220-CMT-Workstation:~/k/k-distribution/tutorial/1_k/5_types/lesson_1$ krun ../../4_imp++/lesson_1/tests/locals.imp --parser 'kast --sort Stmts'
<T> <k> stmt ~> #freezer__0 ( stmt ) ~> #freezer__0 ( stmt ) ~> #freezer__0 ( stmt ) ~> ( x |-> int ) ~> #freezer__1 ( print ( "Line 13: x = " , ( x , ( "\n" , .AExps ) ) ) ;  .Stmts ) ~> #freezer__0 ( stmt ) ~> #freezer__0 ( stmt ) ~> #freezer__0 ( stmt ) ~> ( x |-> int ) ~> #freezer__1 ( print ( "Line 15: x = " , ( x , ( "\n" , .AExps ) ) ) ;  .Stmts ) ~> #freezer__0 ( stmt ) ~> #freezer__0 ( stmt ) ~> #freezer__0 ( stmt ) </k> <tenv> x |-> int </tenv> </T>
yuwen2@yuwen2-HP-Z220-CMT-Workstation:~/k/k-distribution/tutorial/1_k/5_types/lesson_1$ which kompile
/home/yuwen2/k/k-distribution/target/release/k/bin/kompile

Why is the difference?

[cos]

it looks like non-determinism. Could you --search to figure out what's going on?

[andreistefanescu]

I am looking into it. The issue is not one of non-determinism, because stmt should be cooled.