softwarelanguageslab/maf

Non-determinism with duplicate code definitions

Opened this issue · 1 comments

Programs with duplicate definitions (such as test/DEBUG.scm in 10c34dc) seem to have the following issues:

  • The program may be unsound at times, e.g. the daily benchmarks fail sometimes.
  • The error is related to a duplicate definition, which is sometimes bound to bottom by the analysis, but not by the concrete interpreter.

However, even though duplicate definitions exist, this should not lead to unsoundness, and certainly not in a non-deterministic way.

I suppose this is solved now by our new undefiner and the additional restriction that a letrec should not contain duplicate bindings?