1.23
2.0
main
test-branch
|
Last change
on this file since afc300c was 79c4883, checked in by Stephen Siegel <siegel@…>, 10 years ago |
|
Fixed bug in CIVL's evaluation of quantified expressions.
Further work to do to make it better.
Changed test for that bug which did integer division where denominator could be positive or negative. This led to exponential blowup in paths, so not a good test.
Cleaned up some other tests, made them quiter, removed onees that look unnecessary. Fixed some comments.
git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@3779 fb995dde-84ed-4084-dfe6-e5aef3e2452c
|
-
Property mode
set to
100644
|
|
File size:
209 bytes
|
| Line | |
|---|
| 1 | $input int N=5;
|
|---|
| 2 | int m[N][N];
|
|---|
| 3 |
|
|---|
| 4 | int main(){
|
|---|
| 5 | int k;
|
|---|
| 6 |
|
|---|
| 7 | $havoc(&m);
|
|---|
| 8 | $assume($forall (int i, j | 0<=i && i<N && 0<=j && j<N) m[i][j]>0);
|
|---|
| 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.
