[isabelle] Isabelle2021: cvc4 crashing (fixed)



I had been experiencing regular cvc4 crashes (in prior Isabelle versions too, namely 2019 and 2020) when sledgehammer couldn’t find a proof. (crash log below). I found a fix in one of the GitHub issues raised in the cvc5 repo [https://github.com/cvc5/cvc5/pull/6518/files] (this fix was indeed incorporated in cvc5) and managed to carry it over to Isabelle by building cvc4-1.8 from the modified source code and using that binary instead of the default one. This seems OK thus far—I haven’t experienced any crashes. Perhaps the developers could include this in the next release.
++++
Log:

Process:               cvc4 [62181]
Path:                  /Applications/Isabelle2021.app/contrib/cvc4-1.8/x86_64-darwin/cvc4
Identifier:            cvc4
Version:               0
Code Type:             X86-64 (Native)
Parent Process:        ??? [62179]
Responsible:           java [52368]
User ID:               501

Date/Time:             2021-11-15 13:21:08.924 +0100
OS Version:            macOS 11.6 (20G165)
Report Version:        12
Anonymous UUID:        14D42243-651D-5AB4-3D11-CAE3CDF468E0

Sleep/Wake UUID:       73F0573A-597F-44BA-B7B0-70E1C77F6FAF

Time Awake Since Boot: 93000 seconds
Time Since Wake:       12000 seconds

System Integrity Protection: disabled

Crashed Thread:        0  Dispatch queue: com.apple.main-thread

Exception Type:        EXC_CRASH (SIGABRT)
Exception Codes:       0x0000000000000000, 0x0000000000000000
Exception Note:        EXC_CORPSE_NOTIFY

Application Specific Information:
dyld2 mode
abort() called

Thread 0 Crashed:: Dispatch queue: com.apple.main-thread
0   libsystem_kernel.dylib         0x00007fff2038a92e __pthread_kill + 10
1   libsystem_pthread.dylib       0x00007fff203b95bd pthread_kill + 263
2   libsystem_c.dylib             0x00007fff2030e406 abort + 125
3   cvc4                           0x000000010aa0910d CVC4::main::sigint_handler(int, __siginfo*, void*) (.cold.1) + 29
4   cvc4                           0x00000001099f1049 CVC4::main::sigint_handler(int, __siginfo*, void*) + 9
5   libsystem_platform.dylib       0x00007fff203fed7d _sigtramp + 29
6   libsystem_malloc.dylib         0x00007fff201e2f0a tiny_malloc_from_free_list + 555
7   cvc4                           0x000000010a0a9368 CVC4::theory::inst::CandidateGeneratorQE::getNextCandidate() + 936
8   cvc4                           0x000000010a0bd372 CVC4::theory::inst::InstMatchGenerator::getNextMatch(CVC4::NodeTemplate<true>, CVC4::theory::inst::InstMatch&, CVC4::theory::QuantifiersEngine*, CVC4::theory::inst::Trigger*) + 738
9   cvc4                           0x000000010a0bc3b3 CVC4::theory::inst::InstMatchGenerator::continueNextMatch(CVC4::NodeTemplate<true>, CVC4::theory::inst::InstMatch&, CVC4::theory::QuantifiersEngine*, CVC4::theory::inst::Trigger*) + 67
10  cvc4                           0x000000010a0bb797 CVC4::theory::inst::InstMatchGenerator::getMatch(CVC4::NodeTemplate<true>, CVC4::NodeTemplate<true>, CVC4::theory::inst::InstMatch&, CVC4::theory::QuantifiersEngine*, CVC4::theory::inst::Trigger*) + 5687
11  cvc4                           0x000000010a0bd2c2 CVC4::theory::inst::InstMatchGenerator::getNextMatch(CVC4::NodeTemplate<true>, CVC4::theory::inst::InstMatch&, CVC4::theory::QuantifiersEngine*, CVC4::theory::inst::Trigger*) + 562
12  cvc4                           0x000000010a0bc3b3 CVC4::theory::inst::InstMatchGenerator::continueNextMatch(CVC4::NodeTemplate<true>, CVC4::theory::inst::InstMatch&, CVC4::theory::QuantifiersEngine*, CVC4::theory::inst::Trigger*) + 67
13  cvc4                           0x000000010a0bb797 CVC4::theory::inst::InstMatchGenerator::getMatch(CVC4::NodeTemplate<true>, CVC4::NodeTemplate<true>, CVC4::theory::inst::InstMatch&, CVC4::theory::QuantifiersEngine*, CVC4::theory::inst::Trigger*) + 5687
14  cvc4                           0x000000010a0bd2c2 CVC4::theory::inst::InstMatchGenerator::getNextMatch(CVC4::NodeTemplate<true>, CVC4::theory::inst::InstMatch&, CVC4::theory::QuantifiersEngine*, CVC4::theory::inst::Trigger*) + 562
15  cvc4                           0x000000010a0bc3b3 CVC4::theory::inst::InstMatchGenerator::continueNextMatch(CVC4::NodeTemplate<true>, CVC4::theory::inst::InstMatch&, CVC4::theory::QuantifiersEngine*, CVC4::theory::inst::Trigger*) + 67
16  cvc4                           0x000000010a0bb797 CVC4::theory::inst::InstMatchGenerator::getMatch(CVC4::NodeTemplate<true>, CVC4::NodeTemplate<true>, CVC4::theory::inst::InstMatch&, CVC4::theory::QuantifiersEngine*, CVC4::theory::inst::Trigger*) + 5687
17  cvc4                           0x000000010a0bd2c2 CVC4::theory::inst::InstMatchGenerator::getNextMatch(CVC4::NodeTemplate<true>, CVC4::theory::inst::InstMatch&, CVC4::theory::QuantifiersEngine*, CVC4::theory::inst::Trigger*) + 562
18  cvc4                           0x000000010a0bc3b3 CVC4::theory::inst::InstMatchGenerator::continueNextMatch(CVC4::NodeTemplate<true>, CVC4::theory::inst::InstMatch&, CVC4::theory::QuantifiersEngine*, CVC4::theory::inst::Trigger*) + 67
19  cvc4                           0x000000010a0c0701 CVC4::theory::inst::InstMatchGeneratorMultiLinear::getNextMatch(CVC4::NodeTemplate<true>, CVC4::theory::inst::InstMatch&, CVC4::theory::QuantifiersEngine*, CVC4::theory::inst::Trigger*) + 113
20  cvc4                           0x000000010a0bdaac CVC4::theory::inst::InstMatchGenerator::addInstantiations(CVC4::NodeTemplate<true>, CVC4::theory::QuantifiersEngine*, CVC4::theory::inst::Trigger*) + 140
21  cvc4                           0x000000010a0dae33 CVC4::theory::inst::Trigger::addInstantiations() + 51
22  cvc4                           0x000000010a0c9786 CVC4::theory::quantifiers::InstStrategyAutoGenTriggers::process(CVC4::NodeTemplate<true>, CVC4::theory::Theory::Effort, int) + 2214
23  cvc4                           0x000000010a0d7b16 CVC4::theory::quantifiers::InstantiationEngine::doInstantiationRound(CVC4::theory::Theory::Effort) + 262
24  cvc4                           0x000000010a0d8002 CVC4::theory::quantifiers::InstantiationEngine::check(CVC4::theory::Theory::Effort, CVC4::theory::QuantifiersModule::QEffort) + 546
25  cvc4                           0x000000010a31c3df CVC4::theory::QuantifiersEngine::check(CVC4::theory::Theory::Effort) + 1567
26  cvc4                           0x000000010a55f00f CVC4::TheoryEngine::check(CVC4::theory::Theory::Effort) + 1391
27  cvc4                           0x0000000109c03ed1 CVC4::prop::TheoryProxy::theoryCheck(CVC4::theory::Theory::Effort) + 161
28  cvc4                           0x0000000109befa44 CVC4::Minisat::Solver::propagate(CVC4::Minisat::Solver::TheoryCheckType) + 84
29  cvc4                           0x0000000109bf3ab1 CVC4::Minisat::Solver::search(int) + 129
30  cvc4                           0x0000000109bf4938 CVC4::Minisat::Solver::solve_() + 360
31  cvc4                           0x0000000109bfd8a9 CVC4::Minisat::SimpSolver::solve_(bool, bool) + 505
32  cvc4                           0x0000000109bfb017 CVC4::prop::MinisatSatSolver::solve() + 103
33  cvc4                           0x0000000109c02ddd CVC4::prop::PropEngine::checkSat() + 141
34  cvc4                           0x0000000109c47093 CVC4::SmtEngine::check() + 483
35  cvc4                           0x0000000109c49000 CVC4::SmtEngine::checkSatisfiability(std::__1::vector<CVC4::Expr, std::__1::allocator<CVC4::Expr> > const&, bool, bool) + 1264
36  cvc4                           0x0000000109c48823 CVC4::SmtEngine::checkSatisfiability(CVC4::Expr const&, bool, bool) + 179
37  cvc4                           0x0000000109c4870d CVC4::SmtEngine::checkSat(CVC4::Expr const&, bool) + 157
38  cvc4                           0x0000000109c06c26 CVC4::CheckSatCommand::invoke(CVC4::SmtEngine*) + 38
39  cvc4                           0x0000000109c05661 CVC4::Command::invoke(CVC4::SmtEngine*, std::__1::basic_ostream<char, std::__1::char_traits<char> >&) + 33
40  cvc4                           0x00000001099edf97 CVC4::main::smtEngineInvoke(CVC4::SmtEngine*, CVC4::Command*, std::__1::basic_ostream<char, std::__1::char_traits<char> >*) + 39
41  cvc4                           0x00000001099ecea9 CVC4::main::CommandExecutor::doCommandSingleton(CVC4::Command*) + 73
42  cvc4                           0x00000001099ecda5 CVC4::main::CommandExecutor::doCommand(CVC4::Command*) + 293
43  cvc4                           0x00000001099e927b runCvc4(int, char**, CVC4::Options&) + 5947
44  cvc4                           0x00000001099ec611 main + 49
45  libdyld.dylib                 0x00007fff203d4f3d start + 1

Thread 0 crashed with X86 Thread State (64-bit):
  rax: 0x0000000000000000  rbx: 0x0000000119e82e00  rcx: 0x00007ffee6212a58  rdx: 0x0000000000000000
  rdi: 0x0000000000000103  rsi: 0x0000000000000006  rbp: 0x00007ffee6212a80  rsp: 0x00007ffee6212a58
   r8: 0x00007ffee6212f88   r9: 0x73b6e354d7a03e80  r10: 0x0000000000000000  r11: 0x0000000000000246
  r12: 0x0000000000000103  r13: 0x0000000000000000  r14: 0x0000000000000006  r15: 0x0000000000000016
  rip: 0x00007fff2038a92e  rfl: 0x0000000000000246  cr2: 0x000000010aa090f0
 
Logical CPU:     0
Error Code:      0x02000148
Trap Number:     133

Thread 0 instruction stream not available.

Thread 0 last branch register state not available.


Binary Images:
       0x1099e6000 -        0x10ad6dfff +cvc4 (0) <127E97F5-EDB2-3A00-94B8-B5AEB8E9BFE1> /Applications/Isabelle2021.app/contrib/cvc4-1.8/x86_64-darwin/cvc4
       0x119dab000 -        0x119e46fff  dyld (852.2) <0CC19410-FD43-39AE-A32A-50273F8303A4> /usr/lib/dyld
    0x7fff200f1000 -     0x7fff200f2fff  libsystem_blocks.dylib (79) <925E3B6D-184D-3E73-97B1-643C4ADB387A> /usr/lib/system/libsystem_blocks.dylib
    0x7fff200f3000 -     0x7fff20128fff  libxpc.dylib (2038.120.1) <FFFB49D7-2CA6-3E1F-AE4E-5697B19B7D76> /usr/lib/system/libxpc.dylib
    0x7fff20129000 -     0x7fff20140fff  libsystem_trace.dylib (1277.120.1) <7E800ECA-DFDB-3737-A3C5-FFDE37E65383> /usr/lib/system/libsystem_trace.dylib
    0x7fff20141000 -     0x7fff201defff  libcorecrypto.dylib (1000.140.4) <D211160D-E22F-3440-8054-1F5824519C7F> /usr/lib/system/libcorecrypto.dylib
    0x7fff201df000 -     0x7fff2020bfff  libsystem_malloc.dylib (317.140.5) <050E37E1-1458-3F80-BFA3-F1488570169D> /usr/lib/system/libsystem_malloc.dylib
    0x7fff2020c000 -     0x7fff20250fff  libdispatch.dylib (1271.120.2) <8144B0BD-90D2-3EAE-999F-AB0D14082088> /usr/lib/system/libdispatch.dylib
    0x7fff20251000 -     0x7fff2028afff  libobjc.A.dylib (824) <8C7C49A1-4211-3E4C-BA3D-160D675EEE96> /usr/lib/libobjc.A.dylib
    0x7fff2028b000 -     0x7fff2028dfff  libsystem_featureflags.dylib (28.60.1) <E5C43AE3-19E7-3DAB-8B5D-D79A4B68B5C0> /usr/lib/system/libsystem_featureflags.dylib
    0x7fff2028e000 -     0x7fff20316fff  libsystem_c.dylib (1439.141.1) <3C273899-4CBE-32D5-BB31-7A449743204F> /usr/lib/system/libsystem_c.dylib
    0x7fff20317000 -     0x7fff2036cfff  libc++.1.dylib (905.6) <FD6DB1CB-B14B-3404-8BEB-B459C2F6C303> /usr/lib/libc++.1.dylib
    0x7fff2036d000 -     0x7fff20382fff  libc++abi.dylib (905.6) <D0CDDF98-1C04-300F-B685-4A4C59C04C42> /usr/lib/libc++abi.dylib
    0x7fff20383000 -     0x7fff203b2fff  libsystem_kernel.dylib (7195.141.6) <78289AAE-61B5-339F-A485-8819BC2388F2> /usr/lib/system/libsystem_kernel.dylib
    0x7fff203b3000 -     0x7fff203befff  libsystem_pthread.dylib (454.120.2) <1268FF2D-A513-3B51-BA65-AF2FF5789DDB> /usr/lib/system/libsystem_pthread.dylib
    0x7fff203bf000 -     0x7fff203fafff  libdyld.dylib (852.2) <3DE0178A-0AEE-3D08-AE19-6C6403F69BA1> /usr/lib/system/libdyld.dylib
    0x7fff203fb000 -     0x7fff20404fff  libsystem_platform.dylib (254.80.2) <EF52D569-09F5-32E1-B1B3-34E2CA55A017> /usr/lib/system/libsystem_platform.dylib
    0x7fff20405000 -     0x7fff20430fff  libsystem_info.dylib (542.40.3) <55B39B7F-957B-3D99-A8DF-7CA80D38155D> /usr/lib/system/libsystem_info.dylib
    0x7fff22800000 -     0x7fff22809fff  libsystem_darwin.dylib (1439.141.1) <2C81A009-45BB-30D7-A4F7-4B2EEC691617> /usr/lib/system/libsystem_darwin.dylib
    0x7fff22c1f000 -     0x7fff22c2afff  libsystem_notify.dylib (279.40.4) <2E40EA4A-B124-3010-8379-1B4D7082A08F> /usr/lib/system/libsystem_notify.dylib
    0x7fff24bb7000 -     0x7fff24bc5fff  libsystem_networkextension.dylib (1295.140.3) <83AA4425-2F1D-36EC-B77B-8D4F03CDDB68> /usr/lib/system/libsystem_networkextension.dylib
    0x7fff24c24000 -     0x7fff24c3afff  libsystem_asl.dylib (385) <8D324D65-EE16-3A1A-BD39-ACB1B3050D1F> /usr/lib/system/libsystem_asl.dylib
    0x7fff26301000 -     0x7fff26308fff  libsystem_symptoms.dylib (1431.140.1) <1B4D8837-C951-3B69-B079-85D477749E8B> /usr/lib/system/libsystem_symptoms.dylib
    0x7fff28310000 -     0x7fff28320fff  libsystem_containermanager.dylib (318.100.4) <1139CD47-9CBA-356F-8694-1D00EB9F0C8F> /usr/lib/system/libsystem_containermanager.dylib
    0x7fff29024000 -     0x7fff29027fff  libsystem_configuration.dylib (1109.140.1) <02F3A5C9-6289-3012-8F5F-F1DB669ADB79> /usr/lib/system/libsystem_configuration.dylib
    0x7fff29028000 -     0x7fff2902cfff  libsystem_sandbox.dylib (1441.141.4) <5471601B-5072-3E97-8926-804FF08DC4C0> /usr/lib/system/libsystem_sandbox.dylib
    0x7fff29d1e000 -     0x7fff29d20fff  libquarantine.dylib (119.40.2) <3244B57B-9FDF-373E-9F96-A7BAD7534F23> /usr/lib/system/libquarantine.dylib
    0x7fff2a2c9000 -     0x7fff2a2cdfff  libsystem_coreservices.dylib (127.1) <619CCB6D-226C-35BD-98FB-04A18FD54792> /usr/lib/system/libsystem_coreservices.dylib
    0x7fff2a4dd000 -     0x7fff2a524fff  libsystem_m.dylib (3186.100.3) <D61B56FE-649B-34A0-8446-25685B2BBBF2> /usr/lib/system/libsystem_m.dylib
    0x7fff2a526000 -     0x7fff2a52bfff  libmacho.dylib (980) <A4F4D532-7824-3E4E-8FB6-45617415E7DD> /usr/lib/system/libmacho.dylib
    0x7fff2a548000 -     0x7fff2a553fff  libcommonCrypto.dylib (60178.120.3) <CF1E0E70-9F6C-3FAF-82B2-D55F7C9EBB03> /usr/lib/system/libcommonCrypto.dylib
    0x7fff2a554000 -     0x7fff2a55efff  libunwind.dylib (201) <4602E909-C71A-3006-8140-BE616DA241EE> /usr/lib/system/libunwind.dylib
    0x7fff2a55f000 -     0x7fff2a566fff  liboah.dylib (203.58) <F72C2D50-7279-3497-8A59-56908F9661F3> /usr/lib/liboah.dylib
    0x7fff2a567000 -     0x7fff2a571fff  libcopyfile.dylib (173.40.2) <B0F35A80-D5E3-33DD-A47D-ACBFE1300523> /usr/lib/system/libcopyfile.dylib
    0x7fff2a572000 -     0x7fff2a579fff  libcompiler_rt.dylib (102.2) <1C049207-1719-39AC-A2A9-6E5BE28AA138> /usr/lib/system/libcompiler_rt.dylib
    0x7fff2a57a000 -     0x7fff2a57cfff  libsystem_collections.dylib (1439.141.1) <F2D775D9-AAEF-371F-AA54-CFB882B9B430> /usr/lib/system/libsystem_collections.dylib
    0x7fff2a57d000 -     0x7fff2a57ffff  libsystem_secinit.dylib (87.60.1) <EB4516ED-1F8B-3E8A-8C4B-B209A33DCCEF> /usr/lib/system/libsystem_secinit.dylib
    0x7fff2a580000 -     0x7fff2a582fff  libremovefile.dylib (49.120.1) <1AEE3D84-32F9-35FB-8036-B178C9E27D20> /usr/lib/system/libremovefile.dylib
    0x7fff2a583000 -     0x7fff2a583fff  libkeymgr.dylib (31) <698AF6EE-08BB-36CF-B7AD-9EC16E36FA0B> /usr/lib/system/libkeymgr.dylib
    0x7fff2a584000 -     0x7fff2a58bfff  libsystem_dnssd.dylib (1310.140.1) <0685BDB0-9A98-3ADD-B95A-11F221FD80D7> /usr/lib/system/libsystem_dnssd.dylib
    0x7fff2a58c000 -     0x7fff2a591fff  libcache.dylib (83) <B51FAB34-AA9C-38C5-95F1-E5E54B21EA67> /usr/lib/system/libcache.dylib
    0x7fff2a592000 -     0x7fff2a593fff  libSystem.B.dylib (1292.120.1) <DBD0A184-CD98-3225-8E9B-D5BFE0D30562> /usr/lib/libSystem.B.dylib
    0x7fff2d996000 -     0x7fff2d996fff  liblaunch.dylib (2038.120.1) <4A353070-A560-3A98-8869-28C92435C6B2> /usr/lib/system/liblaunch.dylib
    0x7fff2fe2d000 -     0x7fff2fe2dfff  libsystem_product_info_filter.dylib (8.40.1) <78928329-DD98-3799-989D-870DF92FE8D5> /usr/lib/system/libsystem_product_info_filter.dylib

External Modification Summary:
  Calls made by other processes targeting this process:
    task_for_pid: 0
    thread_create: 0
    thread_set_state: 0
  Calls made by this process:
    task_for_pid: 0
    thread_create: 0
    thread_set_state: 0
  Calls made by all processes on this machine:
    task_for_pid: 2
    thread_create: 2
    thread_set_state: 0

VM Region Summary:
ReadOnly portion of Libraries: Total=528.7M resident=0K(0%) swapped_out_or_unallocated=528.7M(100%)
Writable regions: Total=139.9M written=0K(0%) resident=0K(0%) swapped_out=0K(0%) unallocated=139.9M(100%)
 
                                VIRTUAL   REGION
REGION TYPE                        SIZE    COUNT (non-coalesced)
===========                     =======  =======
Kernel Alloc Once                    8K        1
MALLOC                            75.4M       76
MALLOC guard page                   16K        4
MALLOC_LARGE (reserved)            328K        2         reserved VM address space (unallocated)
STACK GUARD                          4K        1
Stack                             64.0M        3
VM_ALLOCATE                          8K        2
__DATA                             500K       44
__DATA_CONST                       334K       34
__DATA_DIRTY                        58K       22
__LINKEDIT                       504.4M        4
__OBJC_RO                         70.3M        1
__OBJC_RW                         2496K        2
__TEXT                            24.4M       44
shared memory                        4K        1
===========                     =======  =======
TOTAL                            742.1M      241
TOTAL, minus reserved VM space   741.7M      241
++++

Regards,
Ujkan Sulejmani



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.