kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

Compiling with the symbolic backend and -superheat option generate not terminating equations #89

Closed dlucanu closed 10 years ago

dlucanu commented 10 years ago

Compile imp.k from dist/tutorial/1_k/4_imp++/lesson_3 with the backend symbolic and superheating the division product:

kompile imp -superheat division -backend symbolic

Then run the program ../lesson_1/div.imp:

$ time krun ../lesson_1/div.imp -cPC true ^C real 2m49.308s user 2m41.764s sys 0m1.386s

As you can see, the execution of the program does not terminate. With the Maude command the execution of the program is ok.

This happens for other languages and programs, too.

andreiarusoaie commented 10 years ago

It was a problem with heating and cooling. Traian fixed it.