Why does the integral work when the lower bound is 0?

[shrey183]

Consider the following SMT2 file,

` (set-logic QF_NRA_ODE)

(declare-fun x () Real)

(declare-fun x_0 () Real [0,10])

(declare-fun x_1 () Real [0,10])

(declare-fun x_2 () Real [0,10])

(declare-fun x_3 () Real [0,10])

(declare-fun time_1 () Real [0,10])

(declare-fun time_2 () Real [0,10])

(define-ode flow_1 ((= d/dt[x] 1)))



(assert (= x_0 0.0))

(assert (= time_1 1.0))

(assert (= time_2 2.0))

(assert
  (and
	;; EXPECT x_1 = 1
	(= [x_1] (integral 0.0 time_1 [x_0] flow_1))

	;; EXPECT x_2 = 2 
	(= [x_2] (integral 1.0 time_2 [x_1] flow_1))

	;; EXPECT x_3 = 0 
	(= [x_3] (integral 1.0 time_1 [x_1] flow_1))
  )
)


(check-sat)

(exit)

`

Here is the model obtained by dReal3,

` delta-sat with the following box:

time_1 : [1, 1];

time_2 : [2, 2];

x_0 : [0, 0];

x_1 : [1, 1];

x_2 : [3, 3];

x_3 : [2, 2]`

I have written comments stating what one should expect each variable to be, though I am not sure why we are getting the above model.