Should be sat but unsat is returned

[shmarovfedor]

I've got the following smt2 file. dReal returns unsat if I use the default -ode_step and sat if I specify the -ode_step (for example, -ode_step=0.1).

(set-logic QF_NRA_ODE)
(declare-fun v () Real)
(declare-fun v_0 () Real)
(declare-fun v_1 () Real)
(declare-fun k () Real)
(declare-fun k_0 () Real)
(declare-fun k_1 () Real)
(declare-fun t () Real)
(declare-fun t_0 () Real)
(declare-fun t_1 () Real)
(declare-fun time_0 () Real)
(define-ode flow_1 ((= d/dt[k] 0.0)(= d/dt[t] 1.0)(= d/dt[v] (* k t))))
(assert (>= v_0 -10000))
(assert (<= v_0 10000))
(assert (>= v_1 -10000))
(assert (<= v_1 10000))
(assert (>= k_0 1.9))
(assert (<= k_0 2.1))
(assert (>= k_1 1.9))
(assert (<= k_1 2.1))
(assert (>= time_0 0))
(assert (<= time_0 17))
(assert (>= t_0 0))
(assert (<= t_0 17))
(assert (>= t_1 0))
(assert (<= t_1 17))
(assert 
(and 
(= [v_1 k_1 t_1] (integral 0. time_0 [v_0 k_0 t_0] flow_1))
(= k_0 k_1)
(= t_0 0)
(>= v_0 0)
(<= v_0 0)
(= t_1 17)
(>= v_1 288.9)
(<= v_1 289.1)
)
)
(check-sat)
(exit)

[shmarovfedor]

It should be sat with k_0 and k_1 close to 2

[soonhokong]

Got it.

[soonhokong]

There was a bug in the split function which generates an interval outside of the domain of computed curve. It led to an exception which caused the problematic behavior. I fixed the bug.

[pzuliani]

Perfect. Thank you!