Assertion violation at third_party/com_github_pinam45_dynamic_bitset/dreal/util/dynamic_bitset.hpp:1942 (--worklist-fixpoint, optimization)

[rainoftime]

Hi, for the following formula,

(set-logic QF_NRA)
(declare-const r2 Real)
(declare-const r4 Real)
(declare-const r12 Real)
(declare-const r16 Real)
(declare-const r31415926 Real)
(declare-const r31415927 Real)
(declare-const r17 Real)
(check-sat)
(assert (or (or (= r16 8.0) (<= r2 0.839583) (or (and (> 22.0 0.0) (= r16 8.0)) (= 0.0 r31415927) (= 0.0 r31415927) (not (= 0.0 r31415927)) (> 474.247 8.0) (and (> 22.0 0.0) (= r16 8.0)) (=> (= 0.0 r31415927) (not (= 0.0 r31415927))) (=> (= 0.0 r31415927) (not (= 0.0 r31415927))) (= r16 8.0)) (not (= 0.0 r31415927)) (not (= 0.0 r31415927)) (> 22.0 (* r17 20.0 r16 1.0)) (> 22.0 (* r17 20.0 r16 1.0)) (or (not (= 0.0 r31415927)) (and (> 22.0 0.0) (= r16 8.0)) (=> (= 0.0 r31415927) (not (= 0.0 r31415927))) (or (= r16 8.0) (not (= 0.0 r31415927))) (or (= r16 8.0) (not (= 0.0 r31415927))) (> 474.247 8.0) (= r16 8.0) (or (= r16 8.0) (not (= 0.0 r31415927))))) (not (= 0.0 r31415927)) (> 474.247 8.0) (=> (= 0.0 r31415927) (not (= 0.0 r31415927))) (= 0.0 r31415927) (<= 438.0 22.0) (not (or (= r16 8.0) (not (= 0.0 r31415927)))) (> 22.0 (* r17 20.0 r16 1.0))))
(assert (or (and (> 22.0 0.0) (= r16 8.0)) (= 0.0 r31415927) (= 0.0 r31415927) (not (= 0.0 r31415927)) (> 474.247 8.0) (and (> 22.0 0.0) (= r16 8.0)) (=> (= 0.0 r31415927) (not (= 0.0 r31415927))) (=> (= 0.0 r31415927) (not (= 0.0 r31415927))) (= r16 8.0)))
(assert (or (= r16 8.0) (or (not (= 0.0 r31415927)) (and (> 22.0 (* r17 20.0 r16 1.0)) (= r16 8.0)) (=> (= 0.0 r31415927) (not (= 0.0 r31415927))) (or (= r16 8.0) (not (= 0.0 r31415927))) (or (= r16 8.0) (not (= 0.0 r31415927))) (> 474.247 8.0) (= r16 8.0) (or (= r16 8.0) (not (= 0.0 r31415927)))) (not (or (= r16 8.0) (not (= 0.0 r31415927)))) (> 474.247 8.0) (< r12 22.0) (<= r2 0.839583) (and (> 22.0 0.0) (= r16 8.0)) (= 0.0 r31415927) (<= 8.0 4.0)))
(minimize (+ r2 r4))
(check-sat)

dreal (commit 215cd00) throws an assertion violation

delta-sat with delta = 0.001
dreal: third_party/com_github_pinam45_dynamic_bitset/dreal/util/dynamic_bitset.hpp:1942: constexpr dreal::dynamic_bitset<Block, Allocator>& dreal::dynamic_bitset<Block, Allocator>::operator|=(const dreal::dynamic_bitset<Block, Allocator>&) [with Block = long unsigned int; Allocator = std::allocator<long unsigned int>]: Assertion `size() >= rhs.size()' failed.

[soonho-tri]

Fixed by be3b52d