No in-between info when using -verbose

[rachelwang]

Why cannot I get any in between info?

../dReal -verbose numodel_3_0.smt2 
unsat

Here is the numodel_3_0.smt2 file:

(set-logic QF_NRA_ODE)
(declare-fun x () Real)
(declare-fun x_0_0 () Real)
(declare-fun x_0_t () Real)
(declare-fun x_1_0 () Real)
(declare-fun x_1_t () Real)
(declare-fun x_2_0 () Real)
(declare-fun x_2_t () Real)
(declare-fun x_3_0 () Real)
(declare-fun x_3_t () Real)
(declare-fun time_0 () Real)
(declare-fun time_1 () Real)
(declare-fun time_2 () Real)
(declare-fun time_3 () Real)
(declare-fun mode_0 () Real)
(declare-fun mode_1 () Real)
(declare-fun mode_2 () Real)
(declare-fun mode_3 () Real)
(define-ode flow_1 ((= d/dt[x] (- 0.000000 (* 0.010000 x)))))
(define-ode flow_2 ((= d/dt[x] (- 1.000000 (* 0.010000 x)))))
(assert (<= 0.000000 x_0_0))
(assert (<= x_0_0 50.000000))
(assert (<= 0.000000 x_0_t))
(assert (<= x_0_t 50.000000))
(assert (<= 0.000000 x_1_0))
(assert (<= x_1_0 50.000000))
(assert (<= 0.000000 x_1_t))
(assert (<= x_1_t 50.000000))
(assert (<= 0.000000 x_2_0))
(assert (<= x_2_0 50.000000))
(assert (<= 0.000000 x_2_t))
(assert (<= x_2_t 50.000000))
(assert (<= 0.000000 x_3_0))
(assert (<= x_3_0 50.000000))
(assert (<= 0.000000 x_3_t))
(assert (<= x_3_t 50.000000))
(assert (<= 0.000000 time_0 [0.000000]))
(assert (<= time_0 1.000000 [0.000000]))
(assert (<= 0.000000 time_1 [0.000000]))
(assert (<= time_1 1.000000 [0.000000]))
(assert (<= 0.000000 time_2 [0.000000]))
(assert (<= time_2 1.000000 [0.000000]))
(assert (<= 0.000000 time_3 [0.000000]))
(assert (<= time_3 1.000000 [0.000000]))
(assert (<= 1.000000 mode_0))
(assert (<= mode_0 2.000000))
(assert (<= 1.000000 mode_1))
(assert (<= mode_1 2.000000))
(assert (<= 1.000000 mode_2))
(assert (<= mode_2 2.000000))
(assert (<= 1.000000 mode_3))
(assert (<= mode_3 2.000000))
(assert (and (= x_0_0 21.000000) (= mode_0 1.000000) (= [x_0_t] (integral 0. time_0 [x_0_0] flow_1)) (= mode_0 1.000000) (forall_t 1.000000 [0.000000 time_0] (>= x_0_t 15.000000)) (>= x_0_t 15.000000) (>= x_0_0 15.000000) (= mode_1 2.000000) (= x_1_0 x_0_t) (< x_0_t 15.000000) (= [x_1_t] (integral 0. time_1 [x_1_0] flow_2)) (= mode_1 2.000000) (forall_t 2.000000 [0.000000 time_1] (<= x_1_t 30.000000)) (<= x_1_t 30.000000) (<= x_1_0 30.000000) (= mode_2 1.000000) (= x_2_0 x_1_t) (> x_1_t 30.000000) (= [x_2_t] (integral 0. time_2 [x_2_0] flow_1)) (= mode_2 1.000000) (forall_t 1.000000 [0.000000 time_2] (>= x_2_t 15.000000)) (>= x_2_t 15.000000) (>= x_2_0 15.000000) (= mode_3 2.000000) (= x_3_0 x_2_t) (< x_2_t 15.000000) (= [x_3_t] (integral 0. time_3 [x_3_0] flow_2)) (= mode_3 2.000000) (forall_t 2.000000 [0.000000 time_3] (<= x_3_t 30.000000)) (<= x_3_t 30.000000) (<= x_3_0 30.000000) (= mode_3 2.000000) (>= x_3_t 18.000000)))
(check-sat)
(exit)

[soonhokong]

You're using strict inequalities and OpenSMT detects a contradiction even before it calls our theory solver.

(assert
 (and
  (< x_0_t 15.000000)
  (< x_2_t 15.000000)
  ...
  (>= x_0_0 15.000000)
  (>= x_0_t 15.000000)
  ...
)

Replacing all the strict inequalities with non-strict ones solves the problem. I still get UNSAT, but it generate log messages with --verbose option. See https://gist.github.com/soonhokong/d2ebb624b4eb35aaa5c4