source: CIVL/examples/reasoning/quantified.cvl

main
Last change on this file was ea777aa, checked in by Alex Wilton <awilton@…>, 3 years ago

Moved examples, include, build_default.properties, common.xml, and README out from dev.civl.com into the root of the repo.

git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@5704 fb995dde-84ed-4084-dfe6-e5aef3e2452c

  • Property mode set to 100644
File size: 209 bytes
RevLine 
[0575b7d]1$input int N=5;
2int m[N][N];
3
4int main(){
5 int k;
6
7 $havoc(&m);
[79c4883]8 $assume($forall (int i, j | 0<=i && i<N && 0<=j && j<N) m[i][j]>0);
[0575b7d]9 for(int i=0; i<N; i++)
10 for(int j=0; j<N; j++)
11 k=1/m[i][j];
12}
Note: See TracBrowser for help on using the repository browser.