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:
651 bytes
|
| Line | |
|---|
| 1 | #include <civlc.cvh>
|
|---|
| 2 |
|
|---|
| 3 | /*
|
|---|
| 4 | Path condition:
|
|---|
| 5 | (0 < -1*(X10[1]*X10[3])+X10[1]*X10[5]+X10[2]*X10[3]+-1*(X10[2]*X10[4])+X10[4]*X10[0]+-1*(X10[5]*X10[0])+-1/115470000000000) &&
|
|---|
| 6 | (0 != 11547/10000*(X10[1]*X10[3])+-11547/10000*(X10[1]*X10[5])+-11547/10000*(X10[2]*X10[3])+11547/10000*(X10[2]*X10[4])+-11547/10000*(X10[4]*X10[0])+11547/10000*(X10[5]*X10[0]))
|
|---|
| 7 | */
|
|---|
| 8 | $input double x[6];
|
|---|
| 9 |
|
|---|
| 10 | int main(){
|
|---|
| 11 | double a = 11547/10000 * (x[1]*x[3] - x[1]*x[5] - x[2]*x[3] + x[2]*x[4] - x[4]*x[0] + x[5]*x[0]);
|
|---|
| 12 | double b = -x[1]*x[3] + x[1]*x[5] + x[2]*x[3] - x[2]*x[4] + x[4]*x[0] - x[5]*x[0] - 1/115470000000000;
|
|---|
| 13 |
|
|---|
| 14 | $assume(0 < b);
|
|---|
| 15 | $assume(0 != a);
|
|---|
| 16 | $assert((a*a) != 0);
|
|---|
| 17 | }
|
|---|
Note:
See
TracBrowser
for help on using the repository browser.
