source: CIVL/examples/reasoning/neqZero.cvl@ ecfe5bf

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

minor correction of time library; added ReasoningTest for tests related to SARL; added a test that reveals a possible bug of SARL: ReasongingTest.neqZero().

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@2067 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 648 bytes
Line 
1#include <civlc.cvh>
2
3/*
4Path 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
10int 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.