dreal4
dreal4 copied to clipboard
std::runtime_error for optimization instance
Hi, for the following optimization instance,
(set-logic QF_NRA)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const r0 Real)
(declare-const r6 Real)
(declare-const r7 Real)
(declare-const r8 Real)
(declare-const r9 Real)
(declare-const v19 Bool)
(declare-const r10 Real)
(declare-const v20 Bool)
(declare-const v21 Bool)
(declare-const v22 Bool)
(declare-const r11 Real)
(declare-const v27 Bool)
(assert (or v5 v18 v18))
(assert (or v19 v12 (or v5 v15 v14 v6 v13 v27 v3 v15)))
(assert (or (or v5 v15 v14 v6 v13 v27 v3 v15) v17 (or v5 v15 v14 v6 v13 v27 v3 v15)))
(assert (or v5 (or v5 v15 v14 v6 v13 v27 v3 v15) v2))
(assert (or v7 v5 v17))
(assert (or v7 v7 v2))
(assert (or v12 v19 v18))
(assert (or v7 v2 v17))
(assert (or v17 v18 v7))
(assert (or v12 v17 (> 3.0 7413753.0)))
(assert (or (> 3.0 7413753.0) (or v5 v15 v14 v6 v13 v27 v3 v15) v5))
(assert (or (>= r9 (/ 0.323 r9)) v5 (or v5 v15 v14 v6 v13 v27 v3 v15)))
(minimize r0)
(maximize r6)
(minimize r8)
(maximize r9)
(check-sat)
dreal4 (Commit 0780274) throws an assertion violation
terminate called after throwing an instance of 'std::runtime_error'
what(): Variable v2_ is of type BOOLEAN and it should not be used to construct a symbolic expression.
Aborted (core dumped)
Strangely, after removing the last objective (maximize r9), dreal can work well.
If there are Boolean variables, and the real invariable occurs in the assertion, then there will be this error