source: CIVL/examples/arithmetic/algebra.cvl@ f3527dd

1.23 2.0 main test-branch
Last change on this file since f3527dd was 3ff27cf, checked in by Manchun Zheng <zmanchun@…>, 11 years ago

updated examples since $assert/$assume has been changed to functions; fixed the model builder for the new side-effect remover.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@2085 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 464 bytes
Line 
1/* Commandline execution:
2 * civl verify algebra.cvl
3 */
4#include <civlc.cvh>
5$input int x;
6$input int y;
7
8void main() {
9 int z0 = x*x + 2*x*y + y*y;
10 int z1 = (x + y) * (x + y);
11 int z2 = x*x - y*y;
12 int z3 = (x + y) * (x - y);
13 int z4 = x*x*x - y*y*y;
14 int z5 = (x - y) * (x*x + x*y + y*y);
15 int z6 = x*x*x + y*y*y;
16 int z7 = (x + y) * (x*x - x*y + y*y);
17
18 $assert((z0 == z1));
19 $assert((z2 == z3));
20 $assert((z4 == z5));
21 $assert((z6 == z7));
22}
Note: See TracBrowser for help on using the repository browser.