ASAN SEGV (partial-triggers + lte-partial-inst + global-negate)

[rainoftime]

Hi,
For this formula:

(set-logic NRA)
(set-option :partial-triggers true)
(set-option :lte-partial-inst true)
(set-option :global-negate true)
(declare-const r0 Real)
(declare-const r7 Real)
(declare-const r13 Real)
(assert (= r13 72765336058 72765336058 (/ r0 r7) 0.098))
(check-sat)

CVC4 compiled with ASAN throws out a SEGV

==70140==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000018 (pc 0x7fb113caf08a bp 0x7ffd1c4f2a00 sp 0x7ffd1c4f29e0 T0)
    #0 0x7fb113caf089 in std::_Rb_tree<CVC4::NodeTemplate<false>, std::pair<CVC4::NodeTemplate<false> const, CVC4::theory::NodeTemplateTrie<false> >, std::_Select1st<std::pair<CVC4::NodeTemplate<false> const, CVC4::theory::NodeTemplateTrie<false> > >, std::less<CVC4::NodeTemplate<false> >, std::allocator<std::pair<CVC4::NodeTemplate<false> const, CVC4::theory::NodeTemplateTrie<false> > > >::begin() /usr/include/c++/5/bits/stl_tree.h:870
    #1 0x7fb113caaff5 in std::map<CVC4::NodeTemplate<false>, CVC4::theory::NodeTemplateTrie<false>, std::less<CVC4::NodeTemplate<false> >, std::allocator<std::pair<CVC4::NodeTemplate<false> const, CVC4::theory::NodeTemplateTrie<false> > > >::begin() /usr/include/c++/5/bits/stl_map.h:339
    #2 0x7fb1140563e7 in CVC4::theory::quantifiers::LtePartialInst::getPartialInstantiations(std::vector<CVC4::NodeTemplate<true>, std::allocator<CVC4::NodeTemplate<true> > >&, CVC4::NodeTemplate<true>, CVC4::NodeTemplate<true>, std::vector<CVC4::NodeTemplate<true>, std::allocator<CVC4::NodeTemplate<true> > >&, std::vector<CVC4::NodeTemplate<true>, std::allocator<CVC4::NodeTemplate<true> > >&, std::vector<CVC4::TypeNode, std::allocator<CVC4::TypeNode> >&, CVC4::theory::NodeTemplateTrie<false>*, unsigned int, unsigned int, unsigned int) /home/peisen/test/tofuzz/CVC4/src/theory/quantifiers/local_theory_ext.cpp:242
    #3 0x7fb1140550d8 in CVC4::theory::quantifiers::LtePartialInst::getInstantiations(std::vector<CVC4::NodeTemplate<true>, std::allocator<CVC4::NodeTemplate<true> > >&) /home/peisen/test/tofuzz/CVC4/src/theory/quantifiers/local_theory_ext.cpp:191
    #4 0x7fb114054151 in CVC4::theory::quantifiers::LtePartialInst::check(CVC4::theory::Theory::Effort, CVC4::theory::QuantifiersModule::QEffort) /home/peisen/test/tofuzz/CVC4/src/theory/quantifiers/local_theory_ext.cpp:138
    #5 0x7fb114386777 in CVC4::theory::QuantifiersEngine::check(CVC4::theory::Theory::Effort) /home/peisen/test/tofuzz/CVC4/src/theory/quantifiers_engine.cpp:705
    #6 0x7fb11437d6f2 in CVC4::theory::quantifiers::TheoryQuantifiers::check(CVC4::theory::Theory::Effort) /home/peisen/test/tofuzz/CVC4/src/theory/quantifiers/theory_quantifiers.cpp:161
    #7 0x7fb114652f57 in CVC4::TheoryEngine::check(CVC4::theory::Theory::Effort) /home/peisen/test/tofuzz/CVC4/src/theory/theory_engine.cpp:608
    #8 0x7fb113628c10 in CVC4::prop::TheoryProxy::theoryCheck(CVC4::theory::Theory::Effort) /home/peisen/test/tofuzz/CVC4/src/prop/theory_proxy.cpp:70
    #9 0x7fb1135d0b40 in CVC4::Minisat::Solver::theoryCheck(CVC4::theory::Theory::Effort) /home/peisen/test/tofuzz/CVC4/src/prop/minisat/core/Solver.cc:1199
    #10 0x7fb1135cfd7c in CVC4::Minisat::Solver::propagate(CVC4::Minisat::Solver::TheoryCheckType) /home/peisen/test/tofuzz/CVC4/src/prop/minisat/core/Solver.cc:1087
    #11 0x7fb1135d2bba in CVC4::Minisat::Solver::search(int) /home/peisen/test/tofuzz/CVC4/src/prop/minisat/core/Solver.cc:1416
    #12 0x7fb1135d4649 in CVC4::Minisat::Solver::solve_() /home/peisen/test/tofuzz/CVC4/src/prop/minisat/core/Solver.cc:1640
    #13 0x7fb11360dc92 in CVC4::Minisat::SimpSolver::solve_(bool, bool) /home/peisen/test/tofuzz/CVC4/src/prop/minisat/simp/SimpSolver.cc:148
    #14 0x7fb113609f34 in CVC4::Minisat::SimpSolver::solve(bool, bool) /home/peisen/test/tofuzz/CVC4/src/./prop/minisat/simp/SimpSolver.h:201
    #15 0x7fb113607d83 in CVC4::prop::MinisatSatSolver::solve() /home/peisen/test/tofuzz/CVC4/src/prop/minisat/minisat.cpp:185
    #16 0x7fb11361ef81 in CVC4::prop::PropEngine::checkSat() /home/peisen/test/tofuzz/CVC4/src/prop/prop_engine.cpp:206

OS: Ubuntu 16.04
Commit: 6a2619c

[ajreynol]

lte-partial-inst was deleted.