Opened 22 months ago
Closed 21 months ago
#66676 closed defect (fixed)
Z3 SMT solver crashes
Reported by: | mouse07410 (Mouse) | Owned by: | catap (Kirill A. Korinsky) |
---|---|---|---|
Priority: | Normal | Milestone: | |
Component: | ports | Version: | |
Keywords: | Cc: | landonf (Landon Fuller) | |
Port: | z3 |
Description
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.
Change History (1)
comment:1 Changed 21 months ago by catap (Kirill A. Korinsky)
Owner: | set to catap |
---|---|
Resolution: | → fixed |
Status: | new → closed |
Note: See
TracTickets for help on using
tickets.
In c307ae9e65c2b65493fe065083b6274edc0ea37d/macports-ports (master):