[MacPorts] #66676: Z3 SMT solver crashes
MacPorts
noreply at macports.org
Thu Jan 12 15:18:50 UTC 2023
#66676: Z3 SMT solver crashes
------------------------+--------------------
Reporter: mouse07410 | Owner: (none)
Type: defect | Status: new
Priority: Normal | Milestone:
Component: ports | Version:
Keywords: | Port: z3
------------------------+--------------------
macOS Monterey 12.6.2, Xcode-14.2.
Reproducer (file {{{test2.smt}}}):
{{{
(set-option :print-success true )
(set-option :produce-models true )
(set-option :global-decls false )
(push 1 )
}}}
Invocation:
{{{
$ z3 -smt2 test2.smt
success
success
success
Segmentation fault: 11
$
}}}
Crash report:
{{{
Termination Reason: Namespace SIGNAL, Code 11 Segmentation fault: 11
Terminating Process: exc handler [58074]
VM Region Info: 0 is not in any region. Bytes before following region:
4382007296
REGION TYPE START - END [ VSIZE] PRT/MAX
SHRMOD REGION DETAIL
UNUSED SPACE AT START
--->
__TEXT 105302000-10689a000 [ 21.6M] r-x/r-x
SM=COW .../local/bin/z3
Thread 0 Crashed:: Dispatch queue: com.apple.main-thread
0 z3 0x106198c80
smt::theory_seq::theory_seq(smt::context&) + 192
1 z3 0x105f55e39
smt::setup::setup_seq_str(static_features const&) + 265
2 z3 0x105f516a0
smt::setup::setup_unknown() + 384
3 z3 0x105ef95e5
smt::context::setup_context(bool) + 149
4 z3 0x105ef570d
smt::context::push() + 61
5 z3 0x105a78908
solver_na2as::push() + 40
6 z3 0x105a9984d
cmd_context::push() + 2205
7 z3 0x105ac6268
smt2::parser::operator()() + 4312
8 z3 0x10672f693
read_smtlib2_commands(char const*) + 563
9 z3 0x10672cfa3 main + 2115
10 dyld 0x10c83352e start + 462
}}}
Also, the current Z3 version released in Sep 2022 is 4.11.2. This port is
still at 4.8.17 - it would be nice to upgrade.
--
Ticket URL: <https://trac.macports.org/ticket/66676>
MacPorts <https://www.macports.org/>
Ports system for macOS
More information about the macports-tickets
mailing list