dreal4 icon indicating copy to clipboard operation
dreal4 copied to clipboard

Assertion violation at symbolic.cc:101 (optimiation instance)

Open rainoftime opened this issue 5 years ago • 0 comments

Hi, for the following formula

(set-logic QF_NRA)
(declare-const r2 Real)
(declare-const r5 Real)
(declare-const r6 Real)
(assert (or (or (>=  6455254657.0 r6) (>=  6455254657.0 r6) (>=  6455254657.0 (- 6.0 6.0))) (or (>=  6455254657.0 (- 6.0 6.0)) (>=  6455254657.0 (- 6.0 6.0)) (>=  6455254657.0 (- 6.0 6.0)))))
(assert (=> (or (>=  6455254657.0 r6) (>=  6455254657.0 r6) (>=  6455254657.0 r6)) (and (or (>=  6455254657.0 (- 6.0 6.0)) (>=  6455254657.0 (- 6.0 6.0)) (>=  6455254657.0 (- 6.0 6.0))) (and (or (>=  6455254657.0 r6) (>=  6455254657.0 r6) (>=  6455254657.0 r6)) (or (>=  6455254657.0 r6) (>=  6455254657.0 r6) (>=  6455254657.0 (- 6.0 6.0))) (or (>=  6455254657.0 (- 6.0 6.0)) (>=  6455254657.0 (- 6.0 6.0)) (>=  6455254657.0 (- 6.0 6.0))) (or (>=  6455254657.0 (- 6.0 6.0)) (>=  6455254657.0 (- 6.0 6.0)) (>=  6455254657.0 (- 6.0 6.0))) (or (>=  6455254657.0 r6) (>=  6455254657.0 r6) (>=  6455254657.0 (- 6.0 6.0)))) (or (>=  6455254657.0 (- 6.0 6.0)) (>=  6455254657.0 (- 6.0 6.0)) (>=  6455254657.0 (- 6.0 6.0))) (and (or (>=  6455254657.0 r6) (>=  6455254657.0 r6) (>=  6455254657.0 r6)) (or (>=  6455254657.0 r6) (>=  6455254657.0 r6) (>=  6455254657.0 (- 6.0 6.0))) (or (>=  6455254657.0 (- 6.0 6.0)) (>=  6455254657.0 (- 6.0 6.0)) (>=  6455254657.0 (- 6.0 6.0))) (or (>=  6455254657.0 (- 6.0 6.0)) (>=  6455254657.0 (- 6.0 6.0)) (>=  6455254657.0 (- 6.0 6.0))) (or (>=  6455254657.0 r6) (>=  6455254657.0 r6) (>=  6455254657.0 (- 6.0 6.0)))) (or (>=  6455254657.0 (- 6.0 6.0)) (>=  6455254657.0 (- 6.0 6.0)) (>=  6455254657.0 (- 6.0 6.0))) (or (>=  6455254657.0 r6) (>=  6455254657.0 r6) (>=  6455254657.0 (- 6.0 6.0))) (or (>=  6455254657.0 (- 6.0 6.0)) (>=  6455254657.0 (- 6.0 6.0)) (>=  6455254657.0 (- 6.0 6.0))))))
(assert (or (>=  6455254657.0 (- 6.0 6.0)) (>=  6455254657.0 r6) (>=  6455254657.0 (- 6.0 6.0))))
(minimize (+ r2 r5))
(minimize (+ r2 r6))
(check-sat)

dreal4 (Commit 0780274) throws an assertion violation

dreal: dreal/symbolic/symbolic.cc:101: std::set<dreal::drake::symbolic::Formula> dreal::get_clauses(const dreal::drake::symbolic::Formula&): Assertion `is_clause(clause)' failed.
Aborted (core dumped)

rainoftime avatar Mar 21 '20 17:03 rainoftime