==14571== Memcheck, a memory error detector ==14571== Copyright (C) 2002-2011, and GNU GPL'd, by Julian Seward et al. ==14571== Using Valgrind-3.7.0 and LibVEX; rerun with -h for copyright info ==14571== Command: builds/bin/.libs/lt-cvc4 rrtest/reachability_back_to_the_future.smt2 -d rewriterules --segv-nospin ==14571== ==14571== Conditional jump or move depends on uninitialised value(s) ==14571== at 0x57A7B69: CVC4::theory::uf::TheoryUF::notifyEqClass(CVC4::NodeTemplate) (theory_uf.cpp:608) ==14571== by 0x57A8C5B: CVC4::theory::uf::TheoryUF::NotifyClass::notifyEqClass(CVC4::NodeTemplate) (theory_uf.h:67) ==14571== by 0x57AEB99: CVC4::theory::uf::EqualityEngine::newNode(CVC4::NodeTemplate, bool) (equality_engine_impl.h:122) ==14571== by 0x57AA93B: CVC4::theory::uf::EqualityEngine::addTerm(CVC4::NodeTemplate) (equality_engine_impl.h:159) ==14571== by 0x57A25BE: CVC4::theory::uf::TheoryUF::TheoryUF(CVC4::context::Context*, CVC4::context::UserContext*, CVC4::theory::OutputChannel&, CVC4::theory::Valuation, CVC4::theory::QuantifiersEngine*) (theory_uf.cpp:48) ==14571== by 0x568E703: void CVC4::TheoryEngine::addTheory(CVC4::theory::TheoryId) (theory_engine.h:525) ==14571== by 0x567C279: CVC4::SmtEngine::SmtEngine(CVC4::ExprManager*) (smt_engine.cpp:273) ==14571== by 0x409673: runCvc4(int, char**, CVC4::Options&) (driver.cpp:156) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Uninitialised value was created by a heap allocation ==14571== at 0x4029447: operator new(unsigned long) (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x568E6B5: void CVC4::TheoryEngine::addTheory(CVC4::theory::TheoryId) (theory_engine.h:525) ==14571== by 0x567C279: CVC4::SmtEngine::SmtEngine(CVC4::ExprManager*) (smt_engine.cpp:273) ==14571== by 0x409673: runCvc4(int, char**, CVC4::Options&) (driver.cpp:156) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 8 ==14571== at 0x553C9C8: CVC4::context::Scope::getContext() const (context.h:285) ==14571== by 0x553CA23: CVC4::context::ContextObj::getContext() const (context.h:561) ==14571== by 0x55FA539: CVC4::context::ContextObj::destroy() (context.cpp:244) ==14571== by 0x5843A60: CVC4::context::CDList >::~CDList() (cdlist.h:262) ==14571== by 0x5840B80: CVC4::theory::arith::ConstraintDatabase::Watches::~Watches() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58391EF: CVC4::theory::arith::ConstraintDatabase::~ConstraintDatabase() (constraint.cpp:507) ==14571== by 0x5891B26: CVC4::theory::arith::TheoryArith::~TheoryArith() (theory_arith.cpp:88) ==14571== by 0x5891EA1: CVC4::theory::arith::TheoryArith::~TheoryArith() (theory_arith.cpp:88) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24d0 is 0 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 4 ==14571== at 0x55FB3C8: CVC4::context::Scope::getLevel() const (context.h:295) ==14571== by 0x55FB4AB: CVC4::context::ContextObj::getLevel() const (context.h:538) ==14571== by 0x55FA54B: CVC4::context::ContextObj::destroy() (context.cpp:243) ==14571== by 0x5843A60: CVC4::context::CDList >::~CDList() (cdlist.h:262) ==14571== by 0x5840B80: CVC4::theory::arith::ConstraintDatabase::Watches::~Watches() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58391EF: CVC4::theory::arith::ConstraintDatabase::~ConstraintDatabase() (constraint.cpp:507) ==14571== by 0x5891B26: CVC4::theory::arith::TheoryArith::~TheoryArith() (theory_arith.cpp:88) ==14571== by 0x5891EA1: CVC4::theory::arith::TheoryArith::~TheoryArith() (theory_arith.cpp:88) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24e0 is 16 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 8 ==14571== at 0x553C9C8: CVC4::context::Scope::getContext() const (context.h:285) ==14571== by 0x553CA23: CVC4::context::ContextObj::getContext() const (context.h:561) ==14571== by 0x55FA7A0: CVC4::context::ContextObj::destroy() (context.cpp:265) ==14571== by 0x5843A60: CVC4::context::CDList >::~CDList() (cdlist.h:262) ==14571== by 0x5840B80: CVC4::theory::arith::ConstraintDatabase::Watches::~Watches() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58391EF: CVC4::theory::arith::ConstraintDatabase::~ConstraintDatabase() (constraint.cpp:507) ==14571== by 0x5891B26: CVC4::theory::arith::TheoryArith::~TheoryArith() (theory_arith.cpp:88) ==14571== by 0x5891EA1: CVC4::theory::arith::TheoryArith::~TheoryArith() (theory_arith.cpp:88) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24d0 is 0 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 8 ==14571== at 0x553C9C8: CVC4::context::Scope::getContext() const (context.h:285) ==14571== by 0x553CA23: CVC4::context::ContextObj::getContext() const (context.h:561) ==14571== by 0x55FA539: CVC4::context::ContextObj::destroy() (context.cpp:244) ==14571== by 0x568C425: CVC4::context::CDHashMap, CVC4::NodeTemplate, CVC4::NodeHashFunction>::~CDHashMap() (cdhashmap.h:318) ==14571== by 0x568B902: CVC4::theory::SubstitutionMap::~SubstitutionMap() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x5891B80: CVC4::theory::arith::TheoryArith::~TheoryArith() (theory_arith.cpp:88) ==14571== by 0x5891EA1: CVC4::theory::arith::TheoryArith::~TheoryArith() (theory_arith.cpp:88) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24d0 is 0 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 4 ==14571== at 0x55FB3C8: CVC4::context::Scope::getLevel() const (context.h:295) ==14571== by 0x55FB4AB: CVC4::context::ContextObj::getLevel() const (context.h:538) ==14571== by 0x55FA54B: CVC4::context::ContextObj::destroy() (context.cpp:243) ==14571== by 0x568C425: CVC4::context::CDHashMap, CVC4::NodeTemplate, CVC4::NodeHashFunction>::~CDHashMap() (cdhashmap.h:318) ==14571== by 0x568B902: CVC4::theory::SubstitutionMap::~SubstitutionMap() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x5891B80: CVC4::theory::arith::TheoryArith::~TheoryArith() (theory_arith.cpp:88) ==14571== by 0x5891EA1: CVC4::theory::arith::TheoryArith::~TheoryArith() (theory_arith.cpp:88) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24e0 is 16 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 8 ==14571== at 0x553C9C8: CVC4::context::Scope::getContext() const (context.h:285) ==14571== by 0x553CA23: CVC4::context::ContextObj::getContext() const (context.h:561) ==14571== by 0x55FA7A0: CVC4::context::ContextObj::destroy() (context.cpp:265) ==14571== by 0x568C425: CVC4::context::CDHashMap, CVC4::NodeTemplate, CVC4::NodeHashFunction>::~CDHashMap() (cdhashmap.h:318) ==14571== by 0x568B902: CVC4::theory::SubstitutionMap::~SubstitutionMap() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x5891B80: CVC4::theory::arith::TheoryArith::~TheoryArith() (theory_arith.cpp:88) ==14571== by 0x5891EA1: CVC4::theory::arith::TheoryArith::~TheoryArith() (theory_arith.cpp:88) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24d0 is 0 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 8 ==14571== at 0x553C9C8: CVC4::context::Scope::getContext() const (context.h:285) ==14571== by 0x553CA23: CVC4::context::ContextObj::getContext() const (context.h:561) ==14571== by 0x55FA539: CVC4::context::ContextObj::destroy() (context.cpp:244) ==14571== by 0x58D8131: CVC4::context::CDHashMap, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::quad, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::theory::arrays::RowLemmaTypeHashFunction>::~CDHashMap() (cdhashmap.h:318) ==14571== by 0x58D5223: CVC4::context::CDHashSet, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::theory::arrays::RowLemmaTypeHashFunction>::~CDHashSet() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58C3DCC: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24d0 is 0 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 4 ==14571== at 0x55FB3C8: CVC4::context::Scope::getLevel() const (context.h:295) ==14571== by 0x55FB4AB: CVC4::context::ContextObj::getLevel() const (context.h:538) ==14571== by 0x55FA54B: CVC4::context::ContextObj::destroy() (context.cpp:243) ==14571== by 0x58D8131: CVC4::context::CDHashMap, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::quad, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::theory::arrays::RowLemmaTypeHashFunction>::~CDHashMap() (cdhashmap.h:318) ==14571== by 0x58D5223: CVC4::context::CDHashSet, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::theory::arrays::RowLemmaTypeHashFunction>::~CDHashSet() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58C3DCC: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24e0 is 16 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid write of size 8 ==14571== at 0x55FA673: CVC4::context::ContextObj::destroy() (context.cpp:254) ==14571== by 0x58D8131: CVC4::context::CDHashMap, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::quad, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::theory::arrays::RowLemmaTypeHashFunction>::~CDHashMap() (cdhashmap.h:318) ==14571== by 0x58D5223: CVC4::context::CDHashSet, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::theory::arrays::RowLemmaTypeHashFunction>::~CDHashSet() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58C3DCC: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24e8 is 24 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 8 ==14571== at 0x553C9C8: CVC4::context::Scope::getContext() const (context.h:285) ==14571== by 0x553CA23: CVC4::context::ContextObj::getContext() const (context.h:561) ==14571== by 0x55FA7A0: CVC4::context::ContextObj::destroy() (context.cpp:265) ==14571== by 0x58D8131: CVC4::context::CDHashMap, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::quad, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::theory::arrays::RowLemmaTypeHashFunction>::~CDHashMap() (cdhashmap.h:318) ==14571== by 0x58D5223: CVC4::context::CDHashSet, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::theory::arrays::RowLemmaTypeHashFunction>::~CDHashSet() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58C3DCC: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24d0 is 0 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 8 ==14571== at 0x553C9C8: CVC4::context::Scope::getContext() const (context.h:285) ==14571== by 0x553CA23: CVC4::context::ContextObj::getContext() const (context.h:561) ==14571== by 0x55FA539: CVC4::context::ContextObj::destroy() (context.cpp:244) ==14571== by 0x58D7F48: CVC4::context::CDList, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::context::DefaultCleanUp, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate > >, std::allocator, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate > > >::~CDList() (cdlist.h:262) ==14571== by 0x58D51B9: CVC4::context::CDQueue, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::context::DefaultCleanUp, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate > >, std::allocator, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate > > >::~CDQueue() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58C3DDE: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24d0 is 0 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 4 ==14571== at 0x55FB3C8: CVC4::context::Scope::getLevel() const (context.h:295) ==14571== by 0x55FB4AB: CVC4::context::ContextObj::getLevel() const (context.h:538) ==14571== by 0x55FA54B: CVC4::context::ContextObj::destroy() (context.cpp:243) ==14571== by 0x58D7F48: CVC4::context::CDList, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::context::DefaultCleanUp, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate > >, std::allocator, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate > > >::~CDList() (cdlist.h:262) ==14571== by 0x58D51B9: CVC4::context::CDQueue, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::context::DefaultCleanUp, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate > >, std::allocator, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate > > >::~CDQueue() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58C3DDE: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24e0 is 16 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid write of size 8 ==14571== at 0x55FA673: CVC4::context::ContextObj::destroy() (context.cpp:254) ==14571== by 0x58D7F48: CVC4::context::CDList, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::context::DefaultCleanUp, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate > >, std::allocator, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate > > >::~CDList() (cdlist.h:262) ==14571== by 0x58D51B9: CVC4::context::CDQueue, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::context::DefaultCleanUp, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate > >, std::allocator, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate > > >::~CDQueue() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58C3DDE: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24e8 is 24 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 8 ==14571== at 0x553C9C8: CVC4::context::Scope::getContext() const (context.h:285) ==14571== by 0x553CA23: CVC4::context::ContextObj::getContext() const (context.h:561) ==14571== by 0x55FA7A0: CVC4::context::ContextObj::destroy() (context.cpp:265) ==14571== by 0x58D7F48: CVC4::context::CDList, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::context::DefaultCleanUp, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate > >, std::allocator, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate > > >::~CDList() (cdlist.h:262) ==14571== by 0x58D51B9: CVC4::context::CDQueue, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate >, CVC4::context::DefaultCleanUp, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate > >, std::allocator, CVC4::NodeTemplate, CVC4::NodeTemplate, CVC4::NodeTemplate > > >::~CDQueue() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58C3DDE: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24d0 is 0 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 8 ==14571== at 0x553C9C8: CVC4::context::Scope::getContext() const (context.h:285) ==14571== by 0x553CA23: CVC4::context::ContextObj::getContext() const (context.h:561) ==14571== by 0x55FA539: CVC4::context::ContextObj::destroy() (context.cpp:244) ==14571== by 0x5733B00: CVC4::context::CDList, CVC4::context::DefaultCleanUp >, std::allocator > >::~CDList() (cdlist.h:262) ==14571== by 0x58C3E92: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24d0 is 0 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 4 ==14571== at 0x55FB3C8: CVC4::context::Scope::getLevel() const (context.h:295) ==14571== by 0x55FB4AB: CVC4::context::ContextObj::getLevel() const (context.h:538) ==14571== by 0x55FA54B: CVC4::context::ContextObj::destroy() (context.cpp:243) ==14571== by 0x5733B00: CVC4::context::CDList, CVC4::context::DefaultCleanUp >, std::allocator > >::~CDList() (cdlist.h:262) ==14571== by 0x58C3E92: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24e0 is 16 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid write of size 8 ==14571== at 0x55FA673: CVC4::context::ContextObj::destroy() (context.cpp:254) ==14571== by 0x5733B00: CVC4::context::CDList, CVC4::context::DefaultCleanUp >, std::allocator > >::~CDList() (cdlist.h:262) ==14571== by 0x58C3E92: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24e8 is 24 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 8 ==14571== at 0x553C9C8: CVC4::context::Scope::getContext() const (context.h:285) ==14571== by 0x553CA23: CVC4::context::ContextObj::getContext() const (context.h:561) ==14571== by 0x55FA7A0: CVC4::context::ContextObj::destroy() (context.cpp:265) ==14571== by 0x5733B00: CVC4::context::CDList, CVC4::context::DefaultCleanUp >, std::allocator > >::~CDList() (cdlist.h:262) ==14571== by 0x58C3E92: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24d0 is 0 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 8 ==14571== at 0x553C9C8: CVC4::context::Scope::getContext() const (context.h:285) ==14571== by 0x553CA23: CVC4::context::ContextObj::getContext() const (context.h:561) ==14571== by 0x55FA539: CVC4::context::ContextObj::destroy() (context.cpp:244) ==14571== by 0x5634CCA: CVC4::context::CDO::~CDO() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58D5F90: CVC4::theory::uf::EqualityEngine::~EqualityEngine() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58C3EA4: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24d0 is 0 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 4 ==14571== at 0x55FB3C8: CVC4::context::Scope::getLevel() const (context.h:295) ==14571== by 0x55FB4AB: CVC4::context::ContextObj::getLevel() const (context.h:538) ==14571== by 0x55FA54B: CVC4::context::ContextObj::destroy() (context.cpp:243) ==14571== by 0x5634CCA: CVC4::context::CDO::~CDO() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58D5F90: CVC4::theory::uf::EqualityEngine::~EqualityEngine() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58C3EA4: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24e0 is 16 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid write of size 8 ==14571== at 0x55FA673: CVC4::context::ContextObj::destroy() (context.cpp:254) ==14571== by 0x5634CCA: CVC4::context::CDO::~CDO() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58D5F90: CVC4::theory::uf::EqualityEngine::~EqualityEngine() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58C3EA4: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24e8 is 24 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 8 ==14571== at 0x553C9C8: CVC4::context::Scope::getContext() const (context.h:285) ==14571== by 0x553CA23: CVC4::context::ContextObj::getContext() const (context.h:561) ==14571== by 0x55FA7A0: CVC4::context::ContextObj::destroy() (context.cpp:265) ==14571== by 0x5634CCA: CVC4::context::CDO::~CDO() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58D5F90: CVC4::theory::uf::EqualityEngine::~EqualityEngine() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58C3EA4: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24d0 is 0 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 8 ==14571== at 0x553C9C8: CVC4::context::Scope::getContext() const (context.h:285) ==14571== by 0x553CA23: CVC4::context::ContextObj::getContext() const (context.h:561) ==14571== by 0x55FA539: CVC4::context::ContextObj::destroy() (context.cpp:244) ==14571== by 0x56FCDEE: CVC4::context::CDO::~CDO() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58D5FC6: CVC4::theory::uf::EqualityEngine::~EqualityEngine() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58C3EA4: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24d0 is 0 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 4 ==14571== at 0x55FB3C8: CVC4::context::Scope::getLevel() const (context.h:295) ==14571== by 0x55FB4AB: CVC4::context::ContextObj::getLevel() const (context.h:538) ==14571== by 0x55FA54B: CVC4::context::ContextObj::destroy() (context.cpp:243) ==14571== by 0x56FCDEE: CVC4::context::CDO::~CDO() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58D5FC6: CVC4::theory::uf::EqualityEngine::~EqualityEngine() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58C3EA4: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24e0 is 16 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid write of size 8 ==14571== at 0x55FA673: CVC4::context::ContextObj::destroy() (context.cpp:254) ==14571== by 0x56FCDEE: CVC4::context::CDO::~CDO() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58D5FC6: CVC4::theory::uf::EqualityEngine::~EqualityEngine() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58C3EA4: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24e8 is 24 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid read of size 8 ==14571== at 0x553C9C8: CVC4::context::Scope::getContext() const (context.h:285) ==14571== by 0x553CA23: CVC4::context::ContextObj::getContext() const (context.h:561) ==14571== by 0x55FA7A0: CVC4::context::ContextObj::destroy() (context.cpp:265) ==14571== by 0x56FCDEE: CVC4::context::CDO::~CDO() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58D5FC6: CVC4::theory::uf::EqualityEngine::~EqualityEngine() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58C3EA4: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24d0 is 0 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid write of size 8 ==14571== at 0x55FA673: CVC4::context::ContextObj::destroy() (context.cpp:254) ==14571== by 0x56FCDEE: CVC4::context::CDO::~CDO() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58D6044: CVC4::theory::uf::EqualityEngine::~EqualityEngine() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58C3EA4: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24e8 is 24 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid write of size 8 ==14571== at 0x55FA673: CVC4::context::ContextObj::destroy() (context.cpp:254) ==14571== by 0x56FCDEE: CVC4::context::CDO::~CDO() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58D607A: CVC4::theory::uf::EqualityEngine::~EqualityEngine() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58C3EA4: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24e8 is 24 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== Invalid write of size 8 ==14571== at 0x55FA673: CVC4::context::ContextObj::destroy() (context.cpp:254) ==14571== by 0x56FCDEE: CVC4::context::CDO::~CDO() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58D609E: CVC4::theory::uf::EqualityEngine::~EqualityEngine() (in /home/bobot/Sources/cvc4/builds/x86_64-unknown-linux-gnu/debug/src/.libs/libcvc4.so.0.0.0) ==14571== by 0x58C3EA4: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:117) ==14571== by 0x58C4219: CVC4::theory::arrays::TheoryArrays::~TheoryArrays() (theory_arrays.cpp:127) ==14571== by 0x56AE6D4: CVC4::TheoryEngine::~TheoryEngine() (theory_engine.cpp:88) ==14571== by 0x567CB2A: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:356) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== Address 0x76f24e8 is 24 bytes inside a block of size 16,384 free'd ==14571== at 0x4028AAE: free (in /usr/lib/valgrind/vgpreload_memcheck-amd64-linux.so) ==14571== by 0x55FCA2B: CVC4::context::ContextMemoryManager::~ContextMemoryManager() (context_mm.cpp:70) ==14571== by 0x55F9415: CVC4::context::Context::~Context() (context.cpp:44) ==14571== by 0x568BE5F: CVC4::context::UserContext::~UserContext() (context.h:210) ==14571== by 0x567CB0D: CVC4::SmtEngine::~SmtEngine() (smt_engine.cpp:354) ==14571== by 0x40A5C7: runCvc4(int, char**, CVC4::Options&) (driver.cpp:323) ==14571== by 0x408B69: main (main.cpp:56) ==14571== ==14571== ==14571== HEAP SUMMARY: ==14571== in use at exit: 48,181 bytes in 595 blocks ==14571== total heap usage: 1,194,994 allocs, 1,194,399 frees, 62,550,725 bytes allocated ==14571== ==14571== LEAK SUMMARY: ==14571== definitely lost: 15,615 bytes in 94 blocks ==14571== indirectly lost: 32,222 bytes in 496 blocks ==14571== possibly lost: 0 bytes in 0 blocks ==14571== still reachable: 344 bytes in 5 blocks ==14571== suppressed: 0 bytes in 0 blocks ==14571== Rerun with --leak-check=full to see details of leaked memory ==14571== ==14571== For counts of detected and suppressed errors, rerun with: -v ==14571== ERROR SUMMARY: 40 errors from 30 contexts (suppressed: 4 from 4)