Session name....... derivativeBad
Directory.......... CIVLREP
Date............... Sun Feb 09 20:50:34 EST 2014
numErrors.......... 1
numDistinctErrors.. 1
search truncated... true

Error 0[length=12, file=CIVLREP/derivativeBad_0.trace]:
CIVL execution error (kind: ASSERTION_VIOLATION, certainty: MAYBE)
Cannot prove assertion holds: $assert(UNIFORM {int k=1..(n-2)} ((*((result+k))-$D[rho, {x,1}]((($real) k*h)))==$O((((h*h)*h)*h))))
  Path condition: (0 == -1*rhox2(0)*(X_s0v1^2)+BIG_O(X_s0v1^3)+rho(-1*X_s0v1)+X_s0v3[1]+-2*X_s0v3[0]) && (0 == -1*rhox2(3*X_s0v1)*(X_s0v1^2)+BIG_O(X_s0v1^3)+rho(4*X_s0v1)+X_s0v3[2]+-2*X_s0v3[3]) && (0 == -1*rhox2(2*X_s0v1)*(X_s0v1^2)+BIG_O(X_s0v1^3)+X_s0v3[1]+-2*X_s0v3[2]+X_s0v3[3]) && (0 == -1*rhox2(X_s0v1)*(X_s0v1^2)+BIG_O(X_s0v1^3)+-2*X_s0v3[1]+X_s0v3[2]+X_s0v3[0]) && (0 == 1/2*rhox2(0)*(X_s0v1^2)+rhox1(0)*X_s0v1+BIG_O(X_s0v1^3)+-1*rho(X_s0v1)+rho(0)) && (0 == 1/2*rhox2(X_s0v1)*(X_s0v1^2)+rhox1(X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+rho(X_s0v1)+-1*rho(2*X_s0v1)) && (0 == 1/2*rhox2(2*X_s0v1)*(X_s0v1^2)+rhox1(2*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+rho(2*X_s0v1)+-1*rho(3*X_s0v1)) && (0 == 1/2*rhox2(3*X_s0v1)*(X_s0v1^2)+rhox1(3*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+rho(3*X_s0v1)+-1*rho(4*X_s0v1)) && (0 == -1*rhox1(0)*X_s0v1+-1/2*rho(-1*X_s0v1)+1/2*X_s0v3[1]) && (0 == -1*rhox1(3*X_s0v1)*X_s0v1+1/2*rho(4*X_s0v1)+-1/2*X_s0v3[2]) && (0 == -1*rhox1(2*X_s0v1)*X_s0v1+-1/2*X_s0v3[1]+1/2*X_s0v3[3]) && (0 == -1*rhox1(X_s0v1)*X_s0v1+1/2*X_s0v3[2]+-1/2*X_s0v3[0]) && (0 <= rhox2(3*X_s0v1)*(X_s0v1^2)+-2*rhox1(3*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*rho(2*X_s0v1)+2*rho(3*X_s0v1)) && (0 <= rhox2(2*X_s0v1)*(X_s0v1^2)+-2*rhox1(2*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*rho(X_s0v1)+2*rho(2*X_s0v1)) && (0 <= rhox2(X_s0v1)*(X_s0v1^2)+-2*rhox1(X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(X_s0v1)+-2*rho(0)) && (0 <= rhox2(0)*(X_s0v1^2)+-2*rhox1(0)*X_s0v1+BIG_O(X_s0v1^3)+-2*rho(-1*X_s0v1)+2*rho(0)) && (0 == -1*rhox2(0)*(X_s0v1^2)+-2*rhox1(0)*X_s0v1+BIG_O(X_s0v1^3)+2*X_s0v3[1]+-2*X_s0v3[0]) && (0 == -1*rhox2(3*X_s0v1)*(X_s0v1^2)+-2*rhox1(3*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(4*X_s0v1)+-2*X_s0v3[3]) && (0 == -1*rhox2(2*X_s0v1)*(X_s0v1^2)+-2*rhox1(2*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*X_s0v3[2]+2*X_s0v3[3]) && (0 == -1*rhox2(X_s0v1)*(X_s0v1^2)+-2*rhox1(X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*X_s0v3[1]+2*X_s0v3[2]) && (0 <= -1*rhox2(3*X_s0v1)*(X_s0v1^2)+-2*rhox1(3*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*rho(3*X_s0v1)+2*rho(4*X_s0v1)) && (0 <= -1*rhox2(2*X_s0v1)*(X_s0v1^2)+-2*rhox1(2*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*rho(2*X_s0v1)+2*rho(3*X_s0v1)) && (0 <= -1*rhox2(X_s0v1)*(X_s0v1^2)+-2*rhox1(X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*rho(X_s0v1)+2*rho(2*X_s0v1)) && (0 <= -1*rhox2(0)*(X_s0v1^2)+-2*rhox1(0)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(X_s0v1)+-2*rho(0)) && (0 <= -1*rhox2(0)*(X_s0v1^2)+-2*rhox1(0)*X_s0v1+BIG_O(X_s0v1^3)+2*X_s0v3[1]+-2*X_s0v3[0]) && (0 <= -1*rhox2(3*X_s0v1)*(X_s0v1^2)+-2*rhox1(3*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(4*X_s0v1)+-2*X_s0v3[3]) && (0 <= -1*rhox2(2*X_s0v1)*(X_s0v1^2)+-2*rhox1(2*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*X_s0v3[2]+2*X_s0v3[3]) && (0 <= -1*rhox2(X_s0v1)*(X_s0v1^2)+-2*rhox1(X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*X_s0v3[1]+2*X_s0v3[2]) && (0 <= -1*rhox2(3*X_s0v1)*(X_s0v1^2)+2*rhox1(3*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(2*X_s0v1)+-2*rho(3*X_s0v1)) && (0 <= -1*rhox2(2*X_s0v1)*(X_s0v1^2)+2*rhox1(2*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(X_s0v1)+-2*rho(2*X_s0v1)) && (0 <= -1*rhox2(X_s0v1)*(X_s0v1^2)+2*rhox1(X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*rho(X_s0v1)+2*rho(0)) && (0 <= -1*rhox2(0)*(X_s0v1^2)+2*rhox1(0)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(-1*X_s0v1)+-2*rho(0)) && (0 == -1*BIG_O(X_s0v1)*X_s0v1+BIG_O(X_s0v1^2)) && (0 == -1*BIG_O(X_s0v1)*(X_s0v1^2)+BIG_O(X_s0v1^3)) && (0 == -1*rho(0)+X_s0v3[0]) && (0 == -1*rho(3*X_s0v1)+X_s0v3[3]) && (0 == -1*rho(2*X_s0v1)+X_s0v3[2]) && (0 == -1*rho(X_s0v1)+X_s0v3[1]) && (0 == 1/2*rhox2(0)*(X_s0v1^2)+-1*rhox1(0)*X_s0v1+BIG_O(X_s0v1^3)+-1*rho(-1*X_s0v1)+rho(0)) && (0 == 1/2*rhox2(X_s0v1)*(X_s0v1^2)+-1*rhox1(X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+rho(X_s0v1)+-1*rho(0)) && (0 == 1/2*rhox2(2*X_s0v1)*(X_s0v1^2)+-1*rhox1(2*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-1*rho(X_s0v1)+rho(2*X_s0v1)) && (0 == 1/2*rhox2(3*X_s0v1)*(X_s0v1^2)+-1*rhox1(3*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-1*rho(2*X_s0v1)+rho(3*X_s0v1)) && (0 < X_s0v1) && (0 <= rhox2(3*X_s0v1)*(X_s0v1^2)+2*rhox1(3*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(3*X_s0v1)+-2*rho(4*X_s0v1)) && (0 <= rhox2(2*X_s0v1)*(X_s0v1^2)+2*rhox1(2*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(2*X_s0v1)+-2*rho(3*X_s0v1)) && (0 <= rhox2(X_s0v1)*(X_s0v1^2)+2*rhox1(X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(X_s0v1)+-2*rho(2*X_s0v1)) && (0 <= rhox2(0)*(X_s0v1^2)+2*rhox1(0)*X_s0v1+BIG_O(X_s0v1^3)+-2*rho(X_s0v1)+2*rho(0)) && (0 <= rhox2(0)*(X_s0v1^2)+2*rhox1(0)*X_s0v1+BIG_O(X_s0v1^3)+-2*X_s0v3[1]+2*X_s0v3[0]) && (0 <= rhox2(3*X_s0v1)*(X_s0v1^2)+2*rhox1(3*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*rho(4*X_s0v1)+2*X_s0v3[3]) && (0 <= rhox2(2*X_s0v1)*(X_s0v1^2)+2*rhox1(2*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*X_s0v3[2]+-2*X_s0v3[3]) && (0 <= rhox2(X_s0v1)*(X_s0v1^2)+2*rhox1(X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*X_s0v3[1]+-2*X_s0v3[2])
  Assertion: (0 == BIG_O(X_s0v1^4)*X_s0v1+rhox1(X_s0v1)*X_s0v1+-1/2*X_s0v3[2]+1/2*X_s0v3[0]) && (0 == BIG_O(X_s0v1^4)*X_s0v1+rhox1(2*X_s0v1)*X_s0v1+1/2*X_s0v3[1]+-1/2*X_s0v3[3])

at f1:27.1-8 "$assert".
State -1:100
| Path condition
| | (0 == -1*rhox2(0)*(X_s0v1^2)+BIG_O(X_s0v1^3)+rho(-1*X_s0v1)+X_s0v3[1]+-2*X_s0v3[0]) && (0 == -1*rhox2(3*X_s0v1)*(X_s0v1^2)+BIG_O(X_s0v1^3)+rho(4*X_s0v1)+X_s0v3[2]+-2*X_s0v3[3]) && (0 == -1*rhox2(2*X_s0v1)*(X_s0v1^2)+BIG_O(X_s0v1^3)+X_s0v3[1]+-2*X_s0v3[2]+X_s0v3[3]) && (0 == -1*rhox2(X_s0v1)*(X_s0v1^2)+BIG_O(X_s0v1^3)+-2*X_s0v3[1]+X_s0v3[2]+X_s0v3[0]) && (0 == 1/2*rhox2(0)*(X_s0v1^2)+rhox1(0)*X_s0v1+BIG_O(X_s0v1^3)+-1*rho(X_s0v1)+rho(0)) && (0 == 1/2*rhox2(X_s0v1)*(X_s0v1^2)+rhox1(X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+rho(X_s0v1)+-1*rho(2*X_s0v1)) && (0 == 1/2*rhox2(2*X_s0v1)*(X_s0v1^2)+rhox1(2*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+rho(2*X_s0v1)+-1*rho(3*X_s0v1)) && (0 == 1/2*rhox2(3*X_s0v1)*(X_s0v1^2)+rhox1(3*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+rho(3*X_s0v1)+-1*rho(4*X_s0v1)) && (0 == -1*rhox1(0)*X_s0v1+-1/2*rho(-1*X_s0v1)+1/2*X_s0v3[1]) && (0 == -1*rhox1(3*X_s0v1)*X_s0v1+1/2*rho(4*X_s0v1)+-1/2*X_s0v3[2]) && (0 == -1*rhox1(2*X_s0v1)*X_s0v1+-1/2*X_s0v3[1]+1/2*X_s0v3[3]) && (0 == -1*rhox1(X_s0v1)*X_s0v1+1/2*X_s0v3[2]+-1/2*X_s0v3[0]) && (0 <= rhox2(3*X_s0v1)*(X_s0v1^2)+-2*rhox1(3*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*rho(2*X_s0v1)+2*rho(3*X_s0v1)) && (0 <= rhox2(2*X_s0v1)*(X_s0v1^2)+-2*rhox1(2*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*rho(X_s0v1)+2*rho(2*X_s0v1)) && (0 <= rhox2(X_s0v1)*(X_s0v1^2)+-2*rhox1(X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(X_s0v1)+-2*rho(0)) && (0 <= rhox2(0)*(X_s0v1^2)+-2*rhox1(0)*X_s0v1+BIG_O(X_s0v1^3)+-2*rho(-1*X_s0v1)+2*rho(0)) && (0 == -1*rhox2(0)*(X_s0v1^2)+-2*rhox1(0)*X_s0v1+BIG_O(X_s0v1^3)+2*X_s0v3[1]+-2*X_s0v3[0]) && (0 == -1*rhox2(3*X_s0v1)*(X_s0v1^2)+-2*rhox1(3*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(4*X_s0v1)+-2*X_s0v3[3]) && (0 == -1*rhox2(2*X_s0v1)*(X_s0v1^2)+-2*rhox1(2*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*X_s0v3[2]+2*X_s0v3[3]) && (0 == -1*rhox2(X_s0v1)*(X_s0v1^2)+-2*rhox1(X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*X_s0v3[1]+2*X_s0v3[2]) && (0 <= -1*rhox2(3*X_s0v1)*(X_s0v1^2)+-2*rhox1(3*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*rho(3*X_s0v1)+2*rho(4*X_s0v1)) && (0 <= -1*rhox2(2*X_s0v1)*(X_s0v1^2)+-2*rhox1(2*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*rho(2*X_s0v1)+2*rho(3*X_s0v1)) && (0 <= -1*rhox2(X_s0v1)*(X_s0v1^2)+-2*rhox1(X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*rho(X_s0v1)+2*rho(2*X_s0v1)) && (0 <= -1*rhox2(0)*(X_s0v1^2)+-2*rhox1(0)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(X_s0v1)+-2*rho(0)) && (0 <= -1*rhox2(0)*(X_s0v1^2)+-2*rhox1(0)*X_s0v1+BIG_O(X_s0v1^3)+2*X_s0v3[1]+-2*X_s0v3[0]) && (0 <= -1*rhox2(3*X_s0v1)*(X_s0v1^2)+-2*rhox1(3*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(4*X_s0v1)+-2*X_s0v3[3]) && (0 <= -1*rhox2(2*X_s0v1)*(X_s0v1^2)+-2*rhox1(2*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*X_s0v3[2]+2*X_s0v3[3]) && (0 <= -1*rhox2(X_s0v1)*(X_s0v1^2)+-2*rhox1(X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*X_s0v3[1]+2*X_s0v3[2]) && (0 <= -1*rhox2(3*X_s0v1)*(X_s0v1^2)+2*rhox1(3*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(2*X_s0v1)+-2*rho(3*X_s0v1)) && (0 <= -1*rhox2(2*X_s0v1)*(X_s0v1^2)+2*rhox1(2*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(X_s0v1)+-2*rho(2*X_s0v1)) && (0 <= -1*rhox2(X_s0v1)*(X_s0v1^2)+2*rhox1(X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*rho(X_s0v1)+2*rho(0)) && (0 <= -1*rhox2(0)*(X_s0v1^2)+2*rhox1(0)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(-1*X_s0v1)+-2*rho(0)) && (0 == -1*BIG_O(X_s0v1)*X_s0v1+BIG_O(X_s0v1^2)) && (0 == -1*BIG_O(X_s0v1)*(X_s0v1^2)+BIG_O(X_s0v1^3)) && (0 == -1*rho(0)+X_s0v3[0]) && (0 == -1*rho(3*X_s0v1)+X_s0v3[3]) && (0 == -1*rho(2*X_s0v1)+X_s0v3[2]) && (0 == -1*rho(X_s0v1)+X_s0v3[1]) && (0 == 1/2*rhox2(0)*(X_s0v1^2)+-1*rhox1(0)*X_s0v1+BIG_O(X_s0v1^3)+-1*rho(-1*X_s0v1)+rho(0)) && (0 == 1/2*rhox2(X_s0v1)*(X_s0v1^2)+-1*rhox1(X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+rho(X_s0v1)+-1*rho(0)) && (0 == 1/2*rhox2(2*X_s0v1)*(X_s0v1^2)+-1*rhox1(2*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-1*rho(X_s0v1)+rho(2*X_s0v1)) && (0 == 1/2*rhox2(3*X_s0v1)*(X_s0v1^2)+-1*rhox1(3*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-1*rho(2*X_s0v1)+rho(3*X_s0v1)) && (0 < X_s0v1) && (0 <= rhox2(3*X_s0v1)*(X_s0v1^2)+2*rhox1(3*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(3*X_s0v1)+-2*rho(4*X_s0v1)) && (0 <= rhox2(2*X_s0v1)*(X_s0v1^2)+2*rhox1(2*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(2*X_s0v1)+-2*rho(3*X_s0v1)) && (0 <= rhox2(X_s0v1)*(X_s0v1^2)+2*rhox1(X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*rho(X_s0v1)+-2*rho(2*X_s0v1)) && (0 <= rhox2(0)*(X_s0v1^2)+2*rhox1(0)*X_s0v1+BIG_O(X_s0v1^3)+-2*rho(X_s0v1)+2*rho(0)) && (0 <= rhox2(0)*(X_s0v1^2)+2*rhox1(0)*X_s0v1+BIG_O(X_s0v1^3)+-2*X_s0v3[1]+2*X_s0v3[0]) && (0 <= rhox2(3*X_s0v1)*(X_s0v1^2)+2*rhox1(3*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+-2*rho(4*X_s0v1)+2*X_s0v3[3]) && (0 <= rhox2(2*X_s0v1)*(X_s0v1^2)+2*rhox1(2*X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*X_s0v3[2]+-2*X_s0v3[3]) && (0 <= rhox2(X_s0v1)*(X_s0v1^2)+2*rhox1(X_s0v1)*X_s0v1+BIG_O(X_s0v1^3)+2*X_s0v3[1]+-2*X_s0v3[2])
| Dynamic scopes
| | dyscope 0 (parent=-1, static=0)
| | | reachers = {0}
| | | variables
| | | | __atomic_lock_var = process<-1>
| | | | h = X_s0v1
| | | | num_elements = 5
| | | | initial = X_s0v3
| | | | working = X_s0v4[0:=(X_s0v3[1]+-1*X_s0v3[0])/X_s0v1, 1:=(1/2*X_s0v3[2]+-1/2*X_s0v3[0])/X_s0v1, 2:=(-1/2*X_s0v3[1]+1/2*X_s0v3[3])/X_s0v1, 3:=(-1/2*X_s0v3[2]+1/2*X_s0v3[4])/X_s0v1, 4:=(-1*X_s0v3[3]+X_s0v3[4])/X_s0v1]
| | dyscope 1 (parent=2, static=4)
| | | reachers = {0}
| | | variables
| | | | i = 4
| | dyscope 2 (parent=0, static=3)
| | | reachers = {0}
| | | variables
| | | | h = X_s0v1
| | | | n = 5
| | | | y = pointer<scope<0>,3,ArrayElementRef(Ref<1>,0)>
| | | | result = pointer<scope<0>,4,ArrayElementRef(Ref<1>,0)>
| Process states
| | process 0
| | | atomicCount = 0
| | | call stack
| | | | Frame[function=differentiate, location=29, f1:27.1-8 "$assert", scope=1]
| | | | Frame[function=_CIVL_system, location=7, f1:31.1-14 "differentiate", scope=0]


