source: CIVL/examples/library/assume.cvl@ cdb0974b

1.23 2.0 acw/focus-triggers main test-branch
Last change on this file since cdb0974b was fded22e, checked in by Manchun Zheng <zmanchun@…>, 11 years ago

added a test for a bug of sarl.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@2064 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 710 bytes
Line 
1// mimic this path condition:
2//(0 < -1*(X2[1]*X2[3])+X2[1]*X2[5]+X2[2]*X2[3]+-1*(X2[2]*X2[4])+X2[4]*X2[0]+-1*(X2[5]*X2[0])+-1/115470000000000)
3//&&
4//(0 != 11547/10000*(X2[1]*X2[3])+-11547/10000*(X2[1]*X2[5])+-11547/10000*(X2[2]*X2[3])+11547/10000*(X2[2]*X2[4])+-11547/10000*(X2[4]*X2[0])+11547/10000*(X2[5]*X2[0]))
5
6#include <civlc.cvh>
7
8$input double a[6];
9
10int main(){
11 double first = - a[1]*a[3] + a[1]*a[5] + a[2]*a[3] - a[2]*a[4] + a[4]*a[0] - a[5]*a[0] - 1/115470000000000;
12
13 $assume (0 < first);
14
15 double second = (a[1]*a[3] - a[1]*a[5] - a[2]*a[3] + a[2]*a[4] - a[4]*a[0] + a[5]*a[0]) * 11547/10000;
16
17 $assume (0 != second);
18
19 for(int i = 0; i <2; i ++)
20 $assume $true;
21
22 $assert $false;
23}
Note: See TracBrowser for help on using the repository browser.