dreal4
dreal4 copied to clipboard
Assertion violation at symbolic.cc:101 (optimiation instance)
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)