segment fault at ibex_mistral_Bitset.h:844 (--worklist-fixpoint)

[rainoftime]

Hi, for the following formula,

(set-logic QF_NRA)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const r0 Real)
(declare-const r1 Real)
(declare-const r2 Real)
(declare-const r3 Real)
(declare-const r7 Real)
(assert (and v1 (<= r2 5.0)))
(assert (and (>= 0.377792885 r7) (<= (sin r0) 0.1031)))
(check-sat)

dreal 662723e throws a segment fault

ASAN:DEADLYSIGNAL
=================================================================
==31311==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000000 (pc 0x563498e2746a bp 0x7ffd43c903b0 sp 0x7ffd43c90390 T0)
==31311==The signal is caused by a READ memory access.
==31311==Hint: address points to the zero page.
    #0 0x563498e27469 in Mistral::Bitset<unsigned int, float>::empty() const external/ibex/include/_opt_libibex_2.7.4_include_ibex/ibex_mistral
_Bitset.h:844
    #1 0x563498e23063 in ibex::BitSet::empty() const external/ibex/include/_opt_libibex_2.7.4_include_ibex/ibex_BitSet.h:324
    #2 0x563498ef37f8 in ibex::BitSet::iterator::iterator(ibex::BitSet const&, bool) external/ibex/include/_opt_libibex_2.7.4_include_ibex/ibex
_BitSet.h:345
    #3 0x563498ef35d1 in ibex::BitSet::begin() const external/ibex/include/_opt_libibex_2.7.4_include_ibex/ibex_BitSet.h:341
    #4 0x563498f0dd42 in dreal::ContractorWorklistFixpoint::Prune(dreal::ContractorStatus*) const dreal/contractor/contractor_worklist_fixpoint
.cc:102
    #5 0x563498ed89b5 in dreal::Contractor::Prune(dreal::ContractorStatus*) const dreal/contractor/contractor.cc:93
    #6 0x563498e3f010 in dreal::IcpSeq::CheckSat(dreal::Contractor const&, std::vector<dreal::FormulaEvaluator, std::allocator<dreal::FormulaEv
aluator> > const&, dreal::ContractorStatus*) dreal/solver/icp_seq.cc:66
    #7 0x563498e4be62 in dreal::TheorySolver::CheckSat(dreal::Box const&, std::vector<dreal::drake::symbolic::Formula, std::allocator<dreal::dr
ake::symbolic::Formula> > const&) dreal/solver/theory_solver.cc:197
    #8 0x563498db3cfc in dreal::Context::Impl::CheckSatCore(dreal::ScopedVector<dreal::drake::symbolic::Formula> const&, dreal::Box, dreal::Sat
Solver*) dreal/solver/context_impl.cc:156
    #9 0x563498db454f in dreal::Context::Impl::CheckSat() dreal/solver/context_impl.cc:184
    #10 0x563498daa1ed in dreal::Context::CheckSat() dreal/solver/context.cc:27
    #11 0x563498d7229c in dreal::Smt2Driver::CheckSat() dreal/smt2/driver.cc:63
    #12 0x563498d78ca3 in dreal::Smt2Parser::parse() dreal/smt2/parser.yy:163
    #13 0x563498d71a73 in dreal::Smt2Driver::parse_stream(std::istream&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocato
r<char> > const&) dreal/smt2/driver.cc:36
    #14 0x563498d71d81 in dreal::Smt2Driver::parse_file(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)
 dreal/smt2/driver.cc:48
    #15 0x563498d75801 in dreal::RunSmt2(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, dreal::Config 
const&, bool, bool) dreal/smt2/run.cc:21
    #16 0x563498bf9fd5 in dreal::MainProgram::Run() dreal/dreal_main.cc:411
    #17 0x563498bfa343 in main dreal/dreal_main.cc:437

[soonho-tri]

Thanks for the report. I'm working on a fix. Subscribe #195 for a follow up.