Non-Terminating Recursion (Prover)

ClemsonRSRG / RESOLVE

RESOLVE (REusable SOftware Language with VErification) is a specification and programming language designed for verifying correctness of object oriented programs.

https://www.cs.clemson.edu/resolve/

BSD 3-Clause "New" or "Revised" License

24 stars 16 forks source link

Non-Terminating Recursion (Prover) #342

Open yushan87 opened 5 years ago

yushan87 commented 5 years ago

Recursion may not terminate... We may have to look at the logs to figure out what is causing it.

https://github.com/ClemsonRSRG/RESOLVE/blob/48b21e528d9d44b4ed9616d7416e28c6e96bd065/src/main/java/edu/clemson/cs/r2jt/congruenceclassprover/TheoremCongruenceClosureImpl.java#L228