Incorrect answer for forall formula with ODEs

[shmarovfedor]

Could you please have a look at this one. dReal returns delta-sat for that one but the expected value is unsat

(set-logic QF_NRA_ODE)
(declare-fun local_time () Real)
(declare-fun local_time_0_0 () Real)
(declare-fun local_time_0_t () Real)
(declare-fun s1 () Real)
(declare-fun s1_0_0 () Real)
(declare-fun s1_0_t () Real)
(assert (>= s1_0_0  0))
(assert (>= s1_0_t  0))
(assert (<= s1_0_0  500))
(assert (<= s1_0_t  500))
(declare-fun s2 () Real)
(declare-fun s2_0_0 () Real)
(declare-fun s2_0_t () Real)
(assert (>= s2_0_0  0))
(assert (>= s2_0_t  0))
(assert (<= s2_0_0  500))
(assert (<= s2_0_t  500))
(declare-fun tau () Real)
(declare-fun tau_0_0 () Real)
(declare-fun tau_0_t () Real)
(assert (>= tau_0_0  0))
(assert (>= tau_0_t  0))
(assert (<= tau_0_0  60))
(assert (<= tau_0_t  60))
(declare-fun v01 () Real)
(declare-fun v01_0_0 () Real)
(declare-fun v01_0_t () Real)
(assert (>= v01_0_0  0))
(assert (>= v01_0_t  0))
(assert (<= v01_0_0  50))
(assert (<= v01_0_t  50))
(declare-fun v02 () Real)
(declare-fun v02_0_0 () Real)
(declare-fun v02_0_t () Real)
(assert (>= v02_0_0  0))
(assert (>= v02_0_t  0))
(assert (<= v02_0_0  50))
(assert (<= v02_0_t  50))
(declare-fun v1 () Real)
(declare-fun v1_0_0 () Real)
(declare-fun v1_0_t () Real)
(assert (>= v1_0_0  0))
(assert (>= v1_0_t  0))
(assert (<= v1_0_0  50))
(assert (<= v1_0_t  50))
(declare-fun v2 () Real)
(declare-fun v2_0_0 () Real)
(declare-fun v2_0_t () Real)
(assert (>= v2_0_0  0))
(assert (>= v2_0_t  0))
(assert (<= v2_0_0  50))
(assert (<= v2_0_t  50))
(declare-fun time_0 () Real)
(assert (>= time_0  0))
(assert (<= time_0  60))
(define-ode flow_1 ((= d/dt[s1] (+ 11.12(* 3 tau)))(= d/dt[s2]  11.12)(= d/dt[tau]  1.0)(= d/dt[v01]  0)(= d/dt[v02]  0)(= d/dt[v1]  3)(= d/dt[v2]  0.0)(= d/dt[local_time] 1.0)))
(assert (and (and 
(or ((and(= s1_0_0 0)(= s2_0_0(* 11.12 2.0))(= v1_0_0 11.12)(= v2_0_0 11.12)(= tau_0_0 0))))
(= [s1_0_t s2_0_t tau_0_t v01_0_t v02_0_t v1_0_t v2_0_t local_time_0_t] (integral 0.0 time_0 [s1_0_0 s2_0_0 tau_0_0 v01_0_0 v02_0_0 v1_0_0 v2_0_0 local_time_0_0] flow_1))
)
(and (forall_t 1 [0 time_0] (not (and (>= s1_0_t(+ s2_0_t(* v2_0_t 2.0)))))))
(= local_time_0_0  0)
(= local_time_0_t  6)
))
(check-sat)
(exit)

[soonho-tri]

I'll check it today.

[soonho-tri]

@shmarovfedor , I simplified the smt2 file and had the following core part. Can you check that this simplification is correct? Mainly, I removed redundant ands, a or, and pushed not into the body of forall_t (by flipping >= to <).

(define-ode flow_1
    ((= d/dt[s1] (+ 11.12(* 3 tau)))
     (= d/dt[s2]  11.12)
     (= d/dt[tau]  1.0)
     (= d/dt[v01]  0)
     (= d/dt[v02]  0)
     (= d/dt[v1]  3)
     (= d/dt[v2]  0.0)
     (= d/dt[local_time] 1.0)))
(assert (and
            (= s1_0_0 0)
            (= s2_0_0 (* 11.12 2.0))
            (= v1_0_0 11.12)
            (= v2_0_0 11.12)
            (= tau_0_0 0)
            (= [s1_0_t s2_0_t tau_0_t v01_0_t v02_0_t v1_0_t v2_0_t local_time_0_t]
                (integral 0.0 time_0 [s1_0_0 s2_0_0 tau_0_0 v01_0_0 v02_0_0 v1_0_0 v2_0_0 local_time_0_0] flow_1))
            (forall_t 1 [0 time_0] (< s1_0_t (+ s2_0_t (* v2_0_t 2.0))))
            (= local_time_0_0  0)
            (= local_time_0_t  6)))

[soonho-tri]

Then, I had delta-sat with the following visualization. Can you check this as well?

[shmarovfedor]

The witness returned by dReal is:

Solution:
local_time_0_0 : [ ENTIRE ] = [0, 0]
local_time_0_t : [ ENTIRE ] = [6, 6]
s1_0_0 : [ ENTIRE ] = [0, 0]
s1_0_t : [ ENTIRE ] = [120.7199999999999, 120.7200000000001]
s2_0_0 : [ ENTIRE ] = [22.24, 22.24]
s2_0_t : [ ENTIRE ] = [88.95999999999995, 88.96000000000002]
tau_0_0 : [ ENTIRE ] = [0, 0]
tau_0_t : [ ENTIRE ] = [5.999999999999997, 6.000000000000003]
time_0 : [ ENTIRE ] = [5.999999999999998, 6.000000000000003]
v01_0_0 : [ ENTIRE ] = [0, 7.275957614183426e-10]
v01_0_t : [ ENTIRE ] = [0, 7.275957614183426e-10]
v02_0_0 : [ ENTIRE ] = [0, 7.275957614183426e-10]
v02_0_t : [ ENTIRE ] = [0, 7.275957614183426e-10]
v1_0_0 : [ ENTIRE ] = [11.12, 11.12]
v1_0_t : [ ENTIRE ] = [29.11999999999999, 29.12000000000002]
v2_0_0 : [ ENTIRE ] = [11.12, 11.12]
v2_0_t : [ ENTIRE ] = [11.12, 11.12]
delta-sat with delta = 0.00000000100000000

However, it violates the forall_t statement. s1_0_t : [ ENTIRE ] = [120.7199999999999, 120.7200000000001], s2_0_t : [ ENTIRE ] = [88.95999999999995, 88.96000000000002] and v2_0_t : [ ENTIRE ] = [11.12, 11.12] and therefore, s1_0_t < (+ s2_0_t (* v2_0_t 2.0)) does not hold (as the left-hand side of the inequality is 120.72 and the right-hand side gives 111.2). So the correct output here would be unsat.

BTW, running this formula without forall_t:

(assert (and
            (= s1_0_0 0)
            (= s2_0_0 (* 11.12 2.0))
            (= v1_0_0 11.12)
            (= v2_0_0 11.12)
            (= tau_0_0 0)
            (= [s1_0_t s2_0_t tau_0_t v01_0_t v02_0_t v1_0_t v2_0_t local_time_0_t]
                (integral 0.0 time_0 [s1_0_0 s2_0_0 tau_0_0 v01_0_0 v02_0_0 v1_0_0 v2_0_0 local_time_0_0] flow_1))
           (< s1_0_t (+ s2_0_t (* v2_0_t 2.0)))
            (= local_time_0_0  0)
            (= local_time_0_t  6)))

returns unsat.

[soonho-tri]

@shmarovfedor : I see. I'll take a closer look.

[soonho-tri]

Found that invariant checking is disabled for this example. Investigating why it happens..

[soonho-tri]

Found the problem and fixed it. A patch will be in the upstream soon.

[soonho-tri]

Closed by 2f564b2d7e9bbc930c67bfa0d5ce023809561447. Thanks for the report, @shmarovfedor !

[pzuliani]

Many thanks @soonho-tri !