// mimic this path condition:
//(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)
//&&
//(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]))

#include <civlc.cvh>

$input double a[6];

int main(){
  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;
 
  $assume((0 < first));

  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;

  $assume((0 != second));

  for(int i = 0; i <2; i ++);
  
  $assert($false);
}