Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2021: cvc4 crashing (fixed)

Email Gateway (Nov 16 2021 at 09:18):

From: Ujkan Sulejmani <ujkan99@gmail.com>
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.dyl
[message truncated]

Email Gateway (Nov 25 2021 at 15:58):

From: Makarius <makarius@sketis.net>
Concerning a cvc4 / cvc5 update, next release means Isabelle2022 (approx.
October 2022).

For Isabelle2021-1 (December 2021) it is too late: We have updated so many
provers for that, but could not revisit cvc4, z3, smbc.

Makarius

Last updated: Apr 19 2024 at 04:17 UTC