Performance hit when adding an "unrelated" variable to optimization problem.

[kunalsheth]

Observation:

Adding an 'unrelated' variable+assertion causes ~50ms linear optimization query to no longer terminate.

Expected Behavior:

I thought dreal_query_FAST.smt2 and dreal_query_SLOW.smt2 would finish in similar amounts of time.

I thought this because variable_X does not impose any additional constraints on the relationship between variable_A and variable_B nor does the minimize expression depend on variable_X.

Actual Behavior:

dreal_query_FAST.smt2:

(set-option :precision 1e-16)

(declare-const variable_X Real)
(declare-const variable_A Real)
(declare-const variable_B Real)

(assert (and (<= variable_B 3) (>= variable_B 0)))
(assert (and (<= variable_A 3) (>= variable_A 0)))

; MAGIC LINE THAT BREAKS THINGS:
; (assert (= variable_X (+ 4e-10 (* 1e-10 variable_B) (* -1e-10 variable_A)) ))
(minimize               (+ 4e-10 (* 1e-10 variable_B) (* -1e-10 variable_A))  )

(check-sat)
(get-model)
(exit)

Result of time cat dreal_query_FAST.smt2 | dreal --in:

delta-sat with delta = 1e-16
(model
  (define-fun variable_X () Real [-4.9999999999999999e-17, 4.9999999999999999e-17])
  (define-fun variable_A () Real 2.9999999998253761)
  (define-fun variable_B () Real [1.7462398116453833e-10, 1.7462408116453831e-10])
)

________________________________________________________
Executed in   39.08 millis    fish           external
   usr time   30.41 millis    0.30 millis   30.11 millis
   sys time   13.56 millis    1.61 millis   11.95 millis

---

dreal_query_SLOW.smt2:

(set-option :precision 1e-16)

(declare-const variable_X Real)
(declare-const variable_A Real)
(declare-const variable_B Real)

(assert (and (<= variable_B 3) (>= variable_B 0)))
(assert (and (<= variable_A 3) (>= variable_A 0)))

; MAGIC LINE THAT BREAKS THINGS:
(assert (= variable_X (+ 4e-10 (* 1e-10 variable_B) (* -1e-10 variable_A)) ))
(minimize             (+ 4e-10 (* 1e-10 variable_B) (* -1e-10 variable_A))  )

(check-sat)
(get-model)
(exit)

Result of time cat dreal_query_SLOW.smt2 | dreal --in:
Nothing- Still running after 30 minutes.