s-falke/llvm2kittel — pull request #25 by jeroenk (2014-04-23 15:20:12+00:00)
Title: Let div and rem return a nondef without constraints

This needs some work before it can be merged. The idea is to provide a coarser abstraction for divisions than the one that is usually used. The coarser abstraction is to generate no constraints at all.

This had some use to me in cases where many div's and rem's occurred, but none were crucial for showing termination.

Problems with the current code:
* This needs a better name than "dumb division"
* This probably works in combination with bounded integers, but it currently does not.

Some feedback on the above issues is more than welcome.