Allow arrays as variables in quantified expressions

team-worthwhile / worthwhile

PSE am KIT 2011/12: Programmverifikation (Team 2)

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

5 stars 3 forks source link

Allow arrays as variables in quantified expressions #70

Closed jspam closed 12 years ago

jspam commented 12 years ago

Since all quantified expressions are evaluated by the prover anyway, we should allow expressions like forall Integer[] x …, which the prover has no problem with.