search

PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
443 stars 93 forks source link

Forward_for and forward_for_simple_bound cannot handle multiple EX in Inv #193

Open QinxiangCao opened 6 years ago

QinxiangCao commented 6 years ago

Forward_for and forward_for_simple_bound cannot handle multiple existential quantifiers in loop invariants.

QinxiangCao commented 6 years ago

Forward_for_simple_bound now allows multiple EX. (PR #260)