Commit 1186e622 authored by Matthew Fernandez's avatar Matthew Fernandez
Browse files

fix generated loop code to iterate correctly

The generated code for a loop (stemming from either a for statement, a forall
expression, or an exists expression) was surprisingly completely broken. When
not iterating over a type (`for x: mytype do ...`) but rather a range
(`for x := 0 to 10 ...`), the generated code would not perform the correct
number of iterations. With ranges not starting from 0, the problem would be
compounded and the value of the loop counter would be incorrect.

This bug was picked up while doing some unrelated work on quantifiers. The fact
that it has never been reported by a user and does not seem to cause any issues
in the test suite or production models leads me to think range-based for loops
are not very common.

Note: down-counting loops (e.g. `10 to 0 by -1`) still do not yet work.

Github: closes #164 "loop iteration code incorrect"
Github: related to #163 "reverse for ranges don't work"
parent e4746dc1
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment